Rocq-Elpi 2.5.0 for Coq 8.20 and Rocq 9.0

What's Changed

• Adapt w.r.t. coq/coq#20060. by @ppedrot in #740
• Adapt to coq/coq#20012 (univgen API change) by @SkySkimmer in #739
• [CI] Update Nix toolbox by @proux01 in #741
• [CI] Use new nicer override mechanism for ocamlPackages.elpi by @proux01 in #743
• document caveat in call-ltac1 by @gares in #745
• Adapt to coq/coq#20095 (record.ml API changes) by @SkySkimmer in #749
• [CI] Remove currently unused file by @proux01 in #751
• Fix #748 (coq.typecheck-indt-decl failing) by @proux01 in #750
• fix(ci.yml): Use coqorg/coq:8.20 as a future-proof image name by @erikmd in #752
• Created rewrite tactic by @patrick-nicodemus in #746
• apply tactic, similar to rewrite by @patrick-nicodemus in #747
• [derive] Add some missing universe constraints by @proux01 in #754
• fix docker ci master by @gares in #753
• [derive.param1] Add some missing universe constraints by @proux01 in #759
• [CI] Add Coq 9.0+rc1 by @proux01 in #757
• Add nicer names in derive.param2 by @proux01 in #761
• Update README.md by @gares in #764
• Add derive.param2.register by @proux01 in #758
• [CI] Readd coqeal by @proux01 in #765
• fix docker ci by @gares in #769
• Adapt to coq/coq#20178 (cominductive API change) by @SkySkimmer in #766
• Fix #766 by @proux01 in #770
• Remove Stdlib dependency by @proux01 in #767
• opam by @gares in #732
• Update coq-elpi.opam by @gares in #772
• Adapt w.r.t. coq/coq#20201. by @ppedrot in #768
• derive: put eqb ast into a namespace by @gares in #731
• Enable compilation without the coq shim on Rocq 9.0 by @proux01 in #771
• fix _CoqProject by @gares in #773
• derive: ability to register an axiom by @gares in #734
• close changelog by @gares in #774

New Contributors

• @erikmd made their first contribution in #752
• @patrick-nicodemus made their first contribution in #746

Full Changelog: v2.4.0...v2.5.0

Coq-Elpi 2.4.0 for Coq 8.20

What's Changed

• Adapt to coq/coq#19530 by @proux01 in #688
• Adapt to coq/coq#19872 (removed auto prop lowering) by @SkySkimmer in #730
• Nix toolbox update by @proux01 in #727
• switch opam ci to docker by @gares in #733
• fix mode signature by @FissoreD in #736
• [CI] Update Nix toolbox by @proux01 in #735
• Adapt w.r.t. coq/coq#19995. by @ppedrot in #738
• Add coq.env.add-context for inserting context declarations by @VojtechStep in #737

New Contributors

• @VojtechStep made their first contribution in #737

Full Changelog: v2.3.0...v2.4.0

Coq-Elpi 2.3.0 for Coq 8.20

What's Changed

• [CI] Fix and test minimal elpi version by @proux01 in #680
• Adapt w.r.t. coq/coq#19481. by @ppedrot in #682
• Overlay for PR 19473 by @mattam82 in #683
• [CI] Add coqeal and Coq 8.20 by @proux01 in #685
• Update doc.yml by @gares in #687
• Fix new compiler by @gares in #692
• drop 8.19 by @gares in #670
• Always resolve files using Coq by @rlepigre in #684
• adapt to coq/coq#19358 by @gares in #668
• fix compilation on 8.20 by @gares in #697
• [TC] premise not run if rigid solution by @FissoreD in #656
• ifdefs on elpi version in source code by @gares in #693
• Update coq-elpi.opam by @gares in #698
• Update version_parser.ml by @gares in #699
• [setup.init] elpi-builtin loaded before coq-builtin by @FissoreD in #700
• Adapt to coq/coq#19620 (Global.push_context_set no strict argument) by @SkySkimmer in #696
• Small typo in documentation by @ckeller in #701
• Adapt to coq/coq#19709 (libobject requires explicit classification) by @SkySkimmer in #702
• remove unused module open by @FissoreD in #705
• [coq_elpi_builtins] change error msg accumulating non-closed clause in a db by @FissoreD in #706
• Fix typo CErrors.error -> user_err by @SkySkimmer in #707
• Fix libobject by @gares in #711
• [CI] Update Nix toolbox by @proux01 in #712
• [CI] Update Nix toolbox by @proux01 in #713
• Support export locality in coq.TC.declare-instance. by @Janno in #715
• Adapt to coq/coq#19584 (record raw ast has loc on idbuild) by @SkySkimmer in #718
• [coq.TC.get-inst-prio] new get-inst-prio (#716) by @FissoreD in #717
• port to Elpi 2.0 by @gares in #719
• example with open terms: extensional replace by @gares in #720
• Improve open by @gares in #723
• typcheck type by @gares in #724
• nix by @gares in #725

New Contributors

• @mattam82 made their first contribution in #683
• @ckeller made their first contribution in #701

Full Changelog: v2.2.3...v2.3.0

Coq-Elpi 2.2.3 for Coq 8.19 and Coq 8.20

What's Changed

• Adapt to coq/coq#19216 by @proux01 in #665
• Adapt to coq/coq#19361 (Lib.*.close_section is incomplete, use Declaremods instead) by @SkySkimmer in #666
• [add-const] do not recompute the uctx for the evar map by @gares in #651
• Fix typos and broken links in tutorials by @wdeweijer in #669
• Adapt to coq/coq#19310 by @proux01 in #662
• Display elpi commands/tactics in the outline by @gares in #667
• Do not escape quotes in verbatim LPDoc documentation. by @ppedrot in #671
• Directly set universes in the global wrapper. by @ppedrot in #672
• dev setup by @gares in #674
• release by @gares in #675

New Contributors

• @wdeweijer made their first contribution in #669

Full Changelog: v2.2.2...v2.2.3

Coq-Elpi 2.2.2 for Coq 8.19 and Coq 8.20

What's Changed

• Don't run tests in build target by @proux01 in #661
• Adapt to coq/coq#19346 (ComInductive flags) by @SkySkimmer in #657
• Update main.yml by @gares in #660
• Update dune-project by @gares in #663
• prepare release by @gares in #664

Full Changelog: v2.2.1...v2.2.2

Coq-Elpi 2.2.1 for Coq 8.19 and 8.20

What's Changed

• TC str2gr conversion not in cache + adapt solve_TC wrt coq hook by @FissoreD in #646
• [derive] Open scope only locally by @eponier in #647
• do not rebuild before installing by @gares in #653
• fix PR #652 by @gares in #654
• adapt to coq/coq#19300 by @gares in #649
• Better error reporting by @gares in #658
• [TC] all tc predicates are inside a tc namespace by @FissoreD in #650
• release by @gares in #659

Full Changelog: v2.2.0...v2.2.1

Coq-Elpi 2.2.0 for Coq 8.19 and Coq 8.20

News

The main changes are:

• the switch to dune allowing for multiple Coq versions to be supported by the same codebase
• the experimental type class solver received a major update

What's Changed

• typos by @FissoreD in #636
• Ho unif with links new by @FissoreD in #629
• [TC] fix compilation of instances in the ctx by @FissoreD in #640
• Port to the [dune] build system. by @rlepigre in #615
• Update coq-nix-toolbox by @vbgl in #641
• remove reglang and deriving jobs by @gares in #642
• support DUNE_FLAGS by @gares in #643
• Better elpitime for benching by @FissoreD in #645
• Add API for projections by @FissoreD in #644

Full Changelog: v2.1.1...v2.2.0

Coq-Elpi 2.1.1 for Coq 8.19

What's Changed

• Fix coq-elpi#618: pick correct initial synterp state in interp phase. by @Janno in #620

Full Changelog: v2.1.0...v2.1.1

Coq-Elpi 2.1.0 for Coq 8.19

What's Changed

• fix: HOAS impargs of record by @gares in #569
• avoid declaring options twice by @gares in #570
• fix detype by @gares in #573
• change error msg when section var are cleared by @FissoreD in #580
• CS app by @Tragicus in #577
• Don't Require PrimInt63 and PrimFloat by default by @proux01 in #579
• fix sigma pruning when calling ltac, reachability is not correct by @gares in #581
• Fix synter impargs by @gares in #583
• Update cs hook by @Tragicus in #593
• Update doc by @proux01 in #599
• API to print a goal by @gares in #602
• attlabel by @gares in #601
• Fix a couple of bugs. by @rlepigre in #605
• Enable loading db from files by @proux01 in #600
• Structured synterp actions by @Janno in #604
• Add synterp phase support for derive plugins. by @rlepigre in #597
• fix uvamp synchronization by @gares in #608
• Enforce correct database initialisation. by @rlepigre in #611
• stash conv problems before typechecking by @Tragicus in #612
• add catches by @Tragicus in #582
• API to fold/unfold primproj by @gares in #521

New Contributors

• @Janno made their first contribution in #604

Full Changelog: v2.0.1...v2.1.0

Coq-Elpi 2.0.2 for Coq 8.19

What's Changed

• fix: HOAS impargs of record by @gares in #569
• avoid declaring options twice by @gares in #570
• fix detype by @gares in #573
• change error msg when section var are cleared by @FissoreD in #580
• CS app by @Tragicus in #577
• Don't Require PrimInt63 and PrimFloat by default by @proux01 in #579
• fix sigma pruning when calling ltac, reachability is not correct by @gares in #581
• Fix synter impargs by @gares in #583
• Update cs hook by @Tragicus in #593

Full Changelog: v2.0.1...v2.0.2