Hierarchy Builder v1.8.1

What's Changed

• [CI] Update Nix toolbox by @proux01 in #491
• fix mode signature by @FissoreD in #492
• Adapt to coq/coq#20028 by @proux01 in #496
• Feature/breaking add section variable by @gares in #497
• fix old coq by @gares in #498
• [CI] Update Nix toolbox by @proux01 in #500
• [CI] Use new nicer override mechanism for ocamlPackages.elpi by @proux01 in #502
• Adapt to LPCIC/coq-elpi#750 by @proux01 in #503
• Revert "Adapt to LPCIC/coq-elpi#750" by @proux01 in #504
• preparing changelog for 1.8.1 by @proux01 in #505

New Contributors

• @FissoreD made their first contribution in #492

Full Changelog: v1.8.0...v1.8.1

Hierarchy Builder v1.8.0

What's Changed

• improve error message missing mixin dep by @gares in #478
• specific error for missing subject by @gares in #479
• detect bogus #[key] attribute by @gares in #480
• Funclass can be dependent by @gares in #483
• improve error message on instance of not a factory by @gares in #481
• HB.instance: failure building a class is not fatal by @gares in #484
• warning if HB.instance does nothing by @gares in #482
• CI update by @proux01 in #489
• Fix test-suite by @proux01 in #488
• Hard failure on missing factories + better error message by @CohenCyril in #487
• preparing changelog for 1.8.0 by @CohenCyril in #490

Full Changelog: v1.7.1...v1.8.0

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.