This version is a variant of MetaRocq 1.5.1 for Rocq 9.1, https://github.com/MetaRocq/metarocq/releases/tag/v1.5.1-9.1 working with Rocq 9.2
What's Changed
- Remove generated file from git repo by @SkySkimmer in #1192
- Adapt to rocq-prover/rocq#21049. by @ppedrot in #1201
- Adapt to rocq-prover/rocq#20614 (induction finds registered schemes) by @SkySkimmer in #1202
- Adapt to Rocq#19987 by @Tragicus in #1152
- Adapt to rocq-prover/rocq#21069 (records can be mutual with non records) by @SkySkimmer in #1205
- Adapt to rocq-prover/rocq#21129. by @ppedrot in #1206
- Adapt to rocq-prover/rocq#21245 (no autogenerated eq_rew schemes) by @SkySkimmer in #1207
- Adapt to rocq-prover/rocq#21193. by @ppedrot in #1217
- Adapt to rocq-prover/rocq#21195 (Univ.ContextSet → PConstraints.ContextSet) by @jrosain in #1216
- Adapt to rocq-prover/rocq#21391. by @ppedrot in #1218
- Adapt to rocq-prover/rocq#21394. by @ppedrot in #1219
- Adapt to rocq-prover/rocq#21384. by @ppedrot in #1220
- Main nix ci and backports by @mattam82 in #1223
- Adapt to rocq-prover/rocq#21419 by @mattam82 in #1224
- Fix issue #1182 (erasure pretty-printer bug for fixpoints) by @mattam82 in #1226
- Adapt to rocq-prover/rocq#21426. by @ppedrot in #1225
- Do not rely on broken universe APIs. by @ppedrot in #1227
- Remove the context set argument from Monomorphic_entry. by @ppedrot in #1228
- Stop using the dubious Rocq type PConstraints.ContextSet.t. by @ppedrot in #1229
- Adapt to rocq-prover/rocq#21486. by @ppedrot in #1232
- Adapt to rocq-prover/rocq#21477 (
Print Assumptionstakes list) by @JasonGross in #1231 - Adapt to rocq-prover/rocq#21438 (PrimRecord record type + has_eta) by @TDiazT in #1230
- Adapt to rocq-prover/rocq#21498 (changed computation uniform parameters) by @thomas-lamiaux in #1233
- Adapt to rocq-prover/rocq#21646 (RegularStyle := MatchStyle) by @SkySkimmer in #1240
- Adapt to rocq-prover/rocq#21669 (evaluable_of_global_reference no env arg) by @SkySkimmer in #1242
- Update main from 9.1 by @mattam82 in #1246
- Bump actions/checkout from 4 to 6 by @dependabot[bot] in #1213
- [9.2] Don't use unguarded
assumptionby @JasonGross in #1275
New Contributors
Full Changelog: v1.5.1-9.1...v1.5.1-9.2