MetaCoq 1.3.4 for Rocq 9.0 (including rc1).
What's Changed
- Remove unused Require Even (Even has been removed from stdlib in 8.19) by @SkySkimmer in #1041
- Update main by @mattam82 in #1044
- Main fixes deprecations by @mattam82 in #1049
- Adapt to coq/coq#18590 by @proux01 in #1055
- Adapt to Coq PR#18397: Declare.declare_variable now takes a "variable_declaration" by @herbelin in #1029
- Adapt to coq/coq#18038 (rewrite rules) by @yannl35133 in #1060
- Adapt to coq/coq#18224 by @proux01 in #1035
- Adapt to coq/coq#18422 (indirect accessor handled through vernactypes) by @SkySkimmer in #1074
- Adapt to coq/coq#18852 (interp_red_expr can be done without ltac) by @SkySkimmer in #1071
- Adapt w.r.t. coq/coq#18910. by @ppedrot in #1076
- Adapt w.r.t. coq/coq#18909. by @ppedrot in #1077
- Adapt to coq PR #18921 fixing bugs of the inference of the return clause for Program-style pattern-matching by @herbelin in #1078
- Adapt to coq/coq#18867 (inductive_sort_family doesn't exist) by @SkySkimmer in #1073
- Adapt to coq/coq#18938 (EConstr.ERelevance) by @SkySkimmer in #1080
- Fixes for funelim by @mattam82 in #1085
- Adapt to Coq PR #18795 (more uniform API for declare.ml) by @herbelin in #1083
- Remove useless calls to Eval vm_compute. by @silene in #1079
- faster PCUICSR by @mrhaandi in #1081
- Adapt to coq/coq#18973. by @rlepigre in #1088
- Remove generated files from archive and ignore them now by @mattam82 in #1092
- Adapt to coq/coq#19384 (add_global_univ -> add_forgotten_univ) by @SkySkimmer in #1096
- Typecheck the result of term unquotation. by @ppedrot in #1098
- Adapt to coq/coq#19310 by @proux01 in #1093
- Correcting the definition of noccur_between in Template – main branch by @MevenBertrand in #1087
- Adapt to coq/coq#19620 (Global.push_context_set no strict argument) by @SkySkimmer in #1104
- Fix quoting and unquoting of primitive strings by @MathisBD in #1109
- Fix quoting and unquoting of primitive strings (#1109) for 8.20 by @yforster in #1110
- Mention 8.20 in DOC.md and INSTALL.md by @yforster in #1121
- metaprogramming library (8.20 version) by @MathisBD in #1122
- Remove bugged option MetaCoq Template Monad Debug. by @SkySkimmer in #1123
- Remove bugged option MetaCoq Template Monad Debug. by @MathisBD in #1126
- Adapt to coq/coq#19530 by @proux01 in #1102
- Update documentation in common/Environment.ml for inductive and constant declarations by @MathisBD in #1128
- Update documentation in common/Environment.ml for inductive and constant declarations by @MathisBD in #1131
- Adapt to coq/coq#19981 (Set Warnings is synterp phase) by @SkySkimmer in #1132
- Adapt w.r.t. coq/coq#19995. by @ppedrot in #1133
- Adapt w.r.t. coq/coq#20060. by @ppedrot in #1134
- Adapt to coq/coq#20095 (record.ml API changes) by @SkySkimmer in #1135
- Adapt to coq/coq#20069 (set_leq_sort doesn't need an env) by @SkySkimmer in #1136
- Adapt to coq/coq#20102 (template poly api change) by @SkySkimmer in #1137
- Merge 8.19 into 8.20 by @yforster in #1138
- Rocq renaming by @mattam82 in #1139
New Contributors
- @silene made their first contribution in #1079
- @rlepigre made their first contribution in #1088
- @MathisBD made their first contribution in #1109
Full Changelog: v1.3.3-8.19...v1.3.4-9.0