Releases: math-comp/hierarchy-builder
Releases · math-comp/hierarchy-builder
Hierarchy Builder 1.10.1
Hierarchy Builder 1.10.0
What's Changed
- Fix makefile by @proux01 in #536
- Refix Makefile by @proux01 in #537
- Drop support for 8.18 and 8.19 by @proux01 in #538
- Cleanup Makefile by @proux01 in #542
- [CI] Add Rocq 9.1 by @proux01 in #546
- port to elpi 3.0 by @gares in #527
- Release by @gares in #550
Full Changelog: v1.9.1...v1.10.0
Hierarchy Builder v1.9.1
What's Changed
- Update AUTHORS.md by @CohenCyril in #532
- remove dead-code by @FissoreD in #533
- Modify
sed
command in the makefile by @KimayaBedarkar in #531 - make: patch all files and only once by @gares in #528
- changed dependency, from coq-elpi to rocq-elpi by @hoheinzollern in #530
New Contributors
- @KimayaBedarkar made their first contribution in #531
- @hoheinzollern made their first contribution in #530
Full Changelog: v1.9.0...v1.9.1
Hierarchy Builder v1.9.0
What's Changed
- Update release script by @proux01 in #506
- [CI] Add Coq 9.0+rc1 by @proux01 in #507
- [CI] Readd coqeal by @proux01 in #508
- [CI] Update Nix toolbox by @proux01 in #509
- Update README.md by @CohenCyril in #511
- Compile without Stdlib by @proux01 in #514
- [CI] Update Nix toolbox by @proux01 in #516
- [CI] Update Nix toolbox by @proux01 in #518
- Backport package from opam repo by @proux01 in #519
- Do not add a mixin-src when there is already one declared by @Tragicus in #522
- Prepare changelog for 1.9.0 by @proux01 in #525
- [CI] Update Docker by @proux01 in #526
New Contributors
Full Changelog: v1.8.1...v1.9.0
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 rocq-prover/rocq#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
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