Compatible with Coq 8.18, 8.19 and 8.20
What's Changed
- improve HB.instance by @gares in #421
- typo addd by @affeldt-aist in #425
- typo addd in tests by @affeldt-aist in #426
- Update nix by @CohenCyril in #424
- HB.saturate: take a cs pattern as a filter by @gares in #414
- make copy-pack-holes failsafe by @gares in #433
- at the end of HB.howto output, it suggests a link to a guide on how to declare mathcomp instances by @Tvallejos in #437
- [CI] Add Coq 8.20 by @proux01 in #439
- put factory-alias->gref in the database by @gares in #445
- Make the code compatible with the new elpi file resolver by @gares in #444
- [CI] Update Nix toolbox by @proux01 in #457
- Disactivate coqeal on master (currently broken) by @proux01 in #458
- [CI] Update Nix toolbox by @proux01 in #461
- port to elpi 2.0 by @gares in #462
- remove typechecking warnings by @gares in #466
- remove buggy notation by @gares in #454
- prepare release by @gares in #470
New Contributors
- @affeldt-aist made their first contribution in #425
- @Tvallejos made their first contribution in #437
Full Changelog: v1.7.0...v1.7.1
Contributors
CohenCyril, gares, and 3 other contributors