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

Coq-Elpi 2.0.0.1 for Coq 8.18

What's Changed

Minor fixes involving ltac calls and programs with a synterp phase.

Full Changelog: v2.0.0...v2.0.0.1

Coq-Elpi 2.0.1 for Coq 8.19

What's Changed

Support for Coq 8.19

New Contributors

• @rlepigre made their first contribution in #502

Full Changelog: v2.0.0...v2.0.1

Coq-Elpi 2.0.0 for Coq 8.18

Requires Elpi 1.18.1 and Coq 8.18.

This major release accommodates for the separation of parsing from execution of Coq 8.18 enabling Coq-Elpi programs to be run efficiently (and correctly) under VSCoq 2.0.

Main changes

• New parsing/execution separation, see the Writing commands in Elpi tutorial
• New (experimental) app tc providing a type-class instance solver

New Contributors

• @Tragicus made their first contribution in #536

Full Changelog: v1.19.3...v2.0.0

Coq-Elpi 1.19.3 for Coq 8.18

What's Changed

• enable λProlog builtins by @phikal in #506
• fix typo by @phikal in #507
• tactic argument for ltac value by @gares in #508
• tutorial: mention @ltacfail! by @gares in #509
• test ocaml 5 by @gares in #510
• example: abstract holes by @gares in #514
• fix location for Elpi Accumulate lp:{{ ... }}. by @gares in #517
• fix separation parsing/execution by @gares in #518

New Contributors

• @phikal made their first contribution in #506

Full Changelog: v1.19.0...v1.19.3

Coq-Elpi 1.19.0 for Coq 8.18

Main novelty is the (experimental) coercion app

Coq-Elpi 1.18.0 for Coq 8.17

Major release. Main change affects typechecking of evars solutions in tactics.