diff --git a/Changelog.md b/Changelog.md index 464d7f1a6..579ff6405 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,11 +1,32 @@ -# Development version +# [2.3.0] - 6/12/2024 + +Requires Elpi 2.0.3 and Coq 8.20. + +The major change is the port to Elpi 2.0 that reports type checking errors +to the location of the offending term and not its exclosing rule. ### Vernacular - `Elpi Accumulate Db Header ` to accumulate just the `Db` declaration but no code added after that +- `Elpi File ` to name a piece of code without + requiring an external file +- `Elpi Accumulate File Signature ` to accumulate only + the types declarations from a file. - `Elpi Typecheck` is deprecated and is a no-op since `Elpi Accumulate` performs type checking incrementally +### HOAS +- new `open-trm` argument for tactics with syntax ````(...)``` and + `ltac_open_term:(...)`. Open terms can mention free variables. +- new `{{:pat ...}}` quotations inside which `_` is interpreted as a + wildcard, not as a regular evar. + +### API +- Support export locality in `coq.TC.declare-instance` +- `tc-instance` now just carries a priority, no matter if inferred or declared, + and works for instances added as `Hint Resolve` to the `typclass_instances` + database + ### Build system - Support dune workspace build with `elpi` diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 6b5a4e2e9..c0853b4c7 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -57,7 +57,7 @@ let rec inlogpath q = function | x :: xs -> (Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs let warning_legacy_typecheck = - CWarnings.create ~default:CWarnings.AsError ~name:"elpi.typecheck-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun () -> + CWarnings.create ~name:"elpi.typecheck-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun () -> Pp.strbrk "The command 'Elpi Typecheck' is deprecated (and does nothing) since type checking is now performed by 'Elpi Accumulate'.") let warning_legacy_accumulate_gen =