Skip to content

rocq 9.2.0#274616

Open
BrewTestBot wants to merge 4 commits intomainfrom
bump-rocq-9.2.0
Open

rocq 9.2.0#274616
BrewTestBot wants to merge 4 commits intomainfrom
bump-rocq-9.2.0

Conversation

@BrewTestBot
Copy link
Copy Markdown
Contributor

@BrewTestBot BrewTestBot commented Mar 27, 2026 •
edited by fxcoudert
Loading

Created by brew bump

Created with brew bump-formula-pr.

  • resource blocks have been checked for updates.

@github-actions github-actions bot added ocaml OCaml use is a significant feature of the PR or issue bump-formula-pr PR was created using `brew bump-formula-pr` labels Mar 27, 2026
@daeho-ro daeho-ro force-pushed the bump-rocq-9.2.0 branch 3 times, most recently from b1d803c to 9ca8a94 Compare March 28, 2026 17:11
@daeho-ro
Copy link
Copy Markdown
Member

daeho-ro commented Mar 28, 2026

From math-comp,

  Error: In term, tolerating this expression at a higher level than expected by
  the notation continuing on the right (which is not left-associative). This
  tolerance will be eventually removed. Insert parentheses or try to lower the
  level at which the top symbol of this expression is parsed.
  [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]
  
  make[2]: *** [Makefile.coq:815: boot/ssrnat.vo] Error 1
  make[2]: *** [boot/ssrnat.vo] Deleting file 'boot/ssrnat.glob'
  make[1]: *** [Makefile.coq:411: all] Error 2
  make: *** [Makefile.common:101: this-build] Error 2

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

bump-formula-pr PR was created using `brew bump-formula-pr` ocaml OCaml use is a significant feature of the PR or issue

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@BrewTestBot @daeho-ro