MetaCoq 1.3.4 for Rocq 9.0

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