Repository navigation

restoring compilation in Rocq 9.4alpha - #256

Merged

nmvdw merged 11 commits into

UniMath:masterfrom

rmatthes:restorecompilationforRocq94alpha

Sep 3, 2026

Merged

restoring compilation in Rocq 9.4alpha#256
nmvdw merged 11 commits into
UniMath:masterfrom
rmatthes:restorecompilationforRocq94alpha

Commits on Sep 2, 2026
- the essential problem is that "is" is now a keyword, the solution is in sync with UniMath PR2083
  rmatthes
  committed
  ae816e0
- add Coq shim to CI
  rmatthes
  committed
  eb38350
- more from UniMath workflow config
  rmatthes
  committed
  d301eec
- try to mend the .yml file
  rmatthes
  committed
  cda4065
- whitespace change
  rmatthes
  committed
  d02ef8b
- Coq 8.16 -> Coq 8.20 in CI
  rmatthes
  committed
  2589cd6
- 8.20 is not recognized in .yml
  rmatthes
  committed
  fae90d3
- gives up on Coq (instead of Rocq)
  rmatthes
  committed
  4401627
- the comment sign is one hash not two
  rmatthes
  committed
  4490043
- whitespace matters
  rmatthes
  committed
  2d434ed
Commits on Sep 3, 2026
- restores compilation by giving more help through terms provided with exact
  rmatthes
  committed
  2720547