Rocq-Elpi 3.4.0 for Rocq 9.0, 9.1 and 9.2
What's Changed
- Xml plugin by @gares in #976
- examples for xml and json by @gares in #977
- separate tests requiring external deps by @gares in #978
- class mode attribute (rocq-prover/rocq#21742) by @FissoreD in #973
- fix observer_evt for old coq version by @FissoreD in #979
- Adapt to rocq-prover/rocq#21680 (wit_tactic top type is tacvalue) by @SkySkimmer in #983
- Fix compilation Rocq 9.2+rc2 by @proux01 in #985
- Adapt to rocq-prover/rocq#21767 (qglobal is not qvar) by @SkySkimmer in #984
- docker ci 9.2 by @gares in #962
- Adapt to rocq-prover/rocq#21820 (collapse_sort_variables arg is not implicit) by @SkySkimmer in #987
- Adapt to rocq-prover/rocq#21811 (Generalize DeclareScheme) by @thomas-lamiaux in #986
- Adapt to rocq-prover/rocq#21851 by @proux01 in #991
- Adapt to rocq-prover/rocq#21901. by @ppedrot in #995
- Elpi 3.7.1 by @gares in #997
- [CI] Update Nix toolbox by @proux01 in #1005
- Adapt to rocq-prover/rocq#21986. by @ppedrot in #1006
- [HOAS] add mutual fixpoints by @gares in #1000
- fix #1007 by @gares in #1008
- Remove no longer used Makefile target by @proux01 in #1009
- [CI] Update Nix toolbox by @proux01 in #1012
- improve API for opening goals by @gares in #1010
derive.param{1,2}: give fresh names to constructors by @t6s in #994- Modifies derive.param2 to translate universe polymorphic terms by @Tvallejos in #1003
- avoid lazy since it seems to dislike memprof_limits by @gares in #1021
- Modifies discriminate.elpi and derive.isK to support univ poly by @Tvallejos in #1018
- Support module types and functors: implement real subst_functions by @JasonGross in #993
- Add coq.env.scheme predicate for looking up registered schemes by @JasonGross in #992
New Contributors
- @t6s made their first contribution in #994
- @Tvallejos made their first contribution in #1003
- @JasonGross made their first contribution in #993
Full Changelog: v3.3.1...v3.4.0