Hierarchy Builder 1.7.1

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

Hierarchy Builder 1.7.0

Compatible with Coq 8.18 with Coq 8.19

What's Changed

• Removed the #[primitive_class] attribute, making it the default.
• New HB.saturate to saturate instances w.r.t. the current hierarchy
• Removed the #[infer] attribute made obsolete by reverse coercions.

Hierarchy Builder 1.6.0

Compatible with Coq 8.16, 8.17 and 8.18.

This release is mainly improving performances in Math Comp 2.0 and Math Comp Analysis.

Hierarchy Builder 1.5.0

Compatible with Coq 8.15, 8.16, 8.17 and 8.18

Hierarchy Builder 1.4.0

Compatible with Coq 8.15 and Coq 8.16.
New features were added, see the Changelog.

Hierarchy Builder 1.3.0

Compatible with Coq 8.15 and Coq 8.16.
New features were added, see the Changelog.

Hierarchy Builder 1.2.1

Minor release adding compatibility with Coq 8.15

Hierarchy Builder 1.2.0

This release works with Coq 8.13 and 8.14 and brings improvements in proof mode.

Hierarchy Builder 1.1.0

Requires Coq 8.11 or 8.12 or 8.13.
This is a major release adding many new features and bugfixes.
See Changelog.md.

Hierarchy Builder 1.0.0

Requires Coq 8.11 or 8.12 or 8.13.

Support for structure parameters and coercions in mixin/factory statements.

See Changelog.