Repository navigation

Full support for Rocq 9.2 - #587

Merged

xavierleroy merged 10 commits into

Jul 21, 2026

Merged

Full support for Rocq 9.2#587
xavierleroy merged 10 commits into
masterfrom
rocq-9.2

Commits on Jul 21, 2026
- Build system: call `rocq` if available, instead of `coqc`, etc
  xavierleroy
  committed
  0ccfd43
- GHA CI: update `latest` action to Rocq 9.2.0
  xavierleroy
  committed
  f5a45f0
- Explicit declaration of proof hints databases using `Create Hintdb`
  xavierleroy
  committed
  f59ceb0
- Rewrite `Proof (term)` as `Proof. exact (term). Qed.`
  xavierleroy
  committed
  4710ec0
- Put postfix notations at level 1
  xavierleroy
  committed
  33244f8
- Avoid `try (rewrite H; auto)` when `H` may not be an equality
  xavierleroy
  committed
  e1e0d42
- Memory.v: use more portable lemmas from ZArith
  xavierleroy
  committed
  b7e9f97
- Makefile: update warning options for Rocq 9.2
  xavierleroy
  committed
  0697626
- MenhirLib/Interpreter.v: reintroduce `Declare Scope` and re-enable warning
  xavierleroy
  committed
  73af265
- Notations `#1` and `#2` (for `fst` and `snd`) moved to Coqlib
  xavierleroy
  committed
  844b397