This release adapts MetaRocq 1.4 to Rocq 9.1. See the previous release notes for this version's main changes.
What's Changed
- Fix test suite overridding COQEXTRAFLAGS by @SkySkimmer in #1141
- Adapt w.r.t. rocq-prover/rocq#20165. by @ppedrot in #1144
- Adapt to rocq-prover/rocq#20178 (UContext.to_context returns qvar set not quality set) by @SkySkimmer in #1145
- Improve evar handling in tmUnquote/tmUnquoteTyped by @MathisBD in #1113
- Adapt w.r.t. rocq-prover/rocq#20278. by @ppedrot in #1147
- Adapt to rocq-prover/rocq#20360 (pr_universe_context_set renamed) by @SkySkimmer in #1150
- CI stop testing ocaml 4.09 (equations needs >= 4.10 now) by @SkySkimmer in #1142
- Update CI for main by @SkySkimmer in #1162
- Adapt for rocq-prover/rocq#20415 by @yannl35133 in #1161
- Fix the proof using a hole in the guard checker by @yannl35133 in #1160
- Adapt to rocq-prover/rocq#20391 (Ltac redef isn't cancelled by importing original module) by @SkySkimmer in #1159
- Take relevance into account for typing by @yannl35133 in #1163
- Nix CI for Rocq-9.0 by @4ever2 in #1164
- Nix CI for main branch by @4ever2 in #1167
- Merge 9.0 in main by @mattam82 in #1170
- Bump cachix/cachix-action from 15 to 16 by @dependabot[bot] in #1168
- Bump cachix/install-nix-action from 30 to 31 by @dependabot[bot] in #1169
- Don't overwrite COQEXTRAFLAGS in test suite by @SkySkimmer in #1171
- Adapt to rocq-prover/rocq#20397 (removal of sort families) by @jrosain in #1172
- Eval erase by @mattam82 in #1173
- adapt to rocq-prover/rocq#20496 (changed bound_names) by @LeoAlexElouan in #1175
- Adapt to rocq-prover/rocq#20603 (moved Lib.section_segment APIs) by @SkySkimmer in #1178
- Adapt to rocq-prover/rocq#20605 (cleaned up projection flags) by @SkySkimmer in #1177
- translations/minihott remove incorrect priority by @SkySkimmer in #1183
- adapt to rocq-prover/rocq#20707 by @gares in #1190
- Adapt to rocq-prover/rocq#20839 (classifier sees ~atts) by @gares in #1191
New Contributors
- @LeoAlexElouan made their first contribution in #1175
Full Changelog: v1.4-9.0...v1.4-9.1