From 553263db8b5b4bb022a95bfb2cfd56386c58c861 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 24 Jan 2024 11:27:24 +0100
Subject: [PATCH 1/6] Strenghten In_size lemma

---
 erasure/theories/EConstructorsAsBlocks.v |  4 +++-
 erasure/theories/EEtaExpanded.v          | 23 +++++++++--------------
 erasure/theories/EEtaExpandedFix.v       |  4 +++-
 erasure/theories/EImplementBox.v         |  8 +++++---
 erasure/theories/ERemoveParams.v         |  5 ++++-
 utils/theories/MCArith.v                 | 23 +++++++++++++++++++++++
 utils/theories/MCList.v                  |  2 +-
 7 files changed, 48 insertions(+), 21 deletions(-)

diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
index 8c5b1621d..ce67f4197 100644
--- a/erasure/theories/EConstructorsAsBlocks.v
+++ b/erasure/theories/EConstructorsAsBlocks.v
@@ -67,7 +67,7 @@ Section transform_blocks.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
     - change (fun x => size (id x)) with size in H.
       eapply (In_size id size) in H. unfold id in H.
       change (fun x => size x) with size in H.
@@ -82,6 +82,8 @@ Section transform_blocks.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in *. lia.
+    - eapply (In_size dbody size) in H; lia.
+    - eapply (In_size dbody size) in H; lia.
     - now eapply InPrim_size in H.
   Qed.
 
diff --git a/erasure/theories/EEtaExpanded.v b/erasure/theories/EEtaExpanded.v
index b8d95c226..a2e6dfa25 100644
--- a/erasure/theories/EEtaExpanded.v
+++ b/erasure/theories/EEtaExpanded.v
@@ -79,23 +79,18 @@ Section isEtaExp.
     | tConstruct ind i block_args => isEtaExp_app ind i 0 && is_nil block_args }.
   Proof.
     all:try lia.
-    all:try apply (In_size); tea.
-    all:try lia.
-    - now apply (In_size id size).
-    - rewrite size_mkApps.
-      eapply (In_size id size) in H.
-      change (fun x => size (id x)) with size in H. unfold id in *; cbn.
-      lia.
-    - now eapply size_mkApps_f.
-    - change (fun x => size (id x)) with size in H.
-      eapply (In_size id size) in H. unfold id in H.
-      change (fun x => size x) with size in H.
-      pose proof (size_mkApps_l napp nnil). lia.
+    3:now eapply size_mkApps_f.
+    3:{ pose proof (size_mkApps_l napp nnil).
+        setoid_rewrite <- (In_size id size H) in H0. unfold id in H0. lia. }
+    all:try rewrite size_mkApps.
+    all:try setoid_rewrite <- (In_size id size H); unfold id.
+    all: try (cbn; lia).
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
     - destruct p as [? []]; cbn in *; intuition eauto.
       subst. lia.
-      eapply (In_size id size) in H0. unfold id in H0.
-      change (fun x => size x) with size in H0. lia.
+      setoid_rewrite <- (In_size id size H0); unfold id. lia.
   Qed.
 
 End isEtaExp.
diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
index ccd7f8bbd..ccd82e884 100644
--- a/erasure/theories/EEtaExpandedFix.v
+++ b/erasure/theories/EEtaExpandedFix.v
@@ -301,7 +301,8 @@ Section isEtaExp.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
+    - setoid_rewrite (In_size id size); tea. unfold id.
+      now change (fun x => size x) with size.
     - rewrite size_mkApps. cbn.
       apply (In_size id size) in H.
       unfold id in H. change (fun x => size x) with size in H. lia.
@@ -320,6 +321,7 @@ Section isEtaExp.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
     - destruct p as [? []]; cbn in *; eauto. destruct H; subst; try lia.
       eapply (In_size id size) in H. unfold id in H.
       change (fun x => size x) with size in H. lia.
diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
index 1dbcbad4f..f6db6a82c 100644
--- a/erasure/theories/EImplementBox.v
+++ b/erasure/theories/EImplementBox.v
@@ -59,9 +59,11 @@ Section implement_box.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
-    - now eapply (In_size id size).
-    - eapply (In_size snd size) in H. cbn in *. lia.
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
+    - setoid_rewrite <- (In_size snd size H); cbn; lia.
+    - setoid_rewrite <- (In_size dbody size H); cbn; lia.
+    - setoid_rewrite <- (In_size dbody size H); cbn; lia.
     - now eapply InPrim_size in H.
   Qed.
 
diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v
index e713de523..f574e2893 100644
--- a/erasure/theories/ERemoveParams.v
+++ b/erasure/theories/ERemoveParams.v
@@ -63,7 +63,8 @@ Section strip.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
-    - now eapply (In_size id size).
+    - eapply (In_size id size) in H. unfold id in H.
+      change (fun x => size x) with size in *. lia.
     - rewrite size_mkApps.
       eapply (In_size id size) in H. change (fun x => size (id x)) with size in H. unfold id in H.  cbn. lia.
     - rewrite size_mkApps.
@@ -72,6 +73,8 @@ Section strip.
     - pose proof (size_mkApps_l napp nnil).
       eapply (In_size id size) in H. change (fun x => size (id x)) with size in H. unfold id in H. lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H; cbn in H; lia.
+    - eapply (In_size dbody size) in H; cbn in H; lia.
     - destruct p as [? []]; cbn in H; eauto.
       intuition auto; subst; cbn; try lia.
       eapply (In_size id size) in H0. unfold id in H0.
diff --git a/utils/theories/MCArith.v b/utils/theories/MCArith.v
index 54c28fa21..b0a076adb 100644
--- a/utils/theories/MCArith.v
+++ b/utils/theories/MCArith.v
@@ -58,3 +58,26 @@ Proof.
   rewrite Pos2Nat.inj_1. reflexivity.
   rewrite Pos2Nat.inj_succ. cbn. f_equal. lia.
 Qed.
+
+(* Missing rewriting theory on natural number orders *)
+
+Require Import Morphisms Morphisms_Prop.
+#[export] Instance proper_S_lt : Morphisms.Proper (lt ==> lt)%signature S.
+Proof. red. intros x y h. lia. Qed.
+#[export] Instance proper_add_lt_r : Morphisms.Proper (eq ==> lt ==> lt)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+#[export] Instance proper_add_lt_l : Morphisms.Proper (lt ==> eq ==> lt)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+
+#[export] Instance proper_S_le : Morphisms.Proper (le ==> le)%signature S.
+Proof. red. intros x y h. lia. Qed.
+#[export] Instance proper_add_le_r : Morphisms.Proper (eq ==> le ==> le)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+#[export] Instance proper_add_le_l : Morphisms.Proper (le ==> eq ==> le)%signature Nat.add.
+Proof. red. intros ??????. lia. Qed.
+
+#[export] Instance subrel_eq_le : subrelation eq le.
+Proof. red. now intros ?? ->. Qed.
+
+#[export] Instance subrel_lt_le : subrelation lt le.
+Proof. red. intros ???. lia. Qed.
diff --git a/utils/theories/MCList.v b/utils/theories/MCList.v
index 125f70869..c8cff4db1 100644
--- a/utils/theories/MCList.v
+++ b/utils/theories/MCList.v
@@ -1406,7 +1406,7 @@ Proof.
 Qed.
 
 Lemma In_size {A B} {x : A} {l : list A} (proj : A -> B) (size : B -> nat) :
-  In x l -> size (proj x) < S (list_size (size ∘ proj) l).
+  In x l -> size (proj x) < (list_size (size ∘ proj) l).
 Proof.
   induction l; cbn => //.
   intros [->|hin]. lia. specialize (IHl hin); lia.

From ec3d756d5b05d11bbb11c4a1c202be3bbf1dfb01 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 24 Jan 2024 09:05:23 -0800
Subject: [PATCH 2/6] Restore compatibility with OCaml < 4.13 (#1023)

Fixes #1022 after #998
---
 template-coq/src/denoter.ml |  2 +-
 template-coq/src/quoter.ml  |  2 +-
 template-coq/src/tm_util.ml | 17 +++++++++++++++++
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml
index bfb34c032..9d34d1e77 100644
--- a/template-coq/src/denoter.ml
+++ b/template-coq/src/denoter.ml
@@ -163,7 +163,7 @@ struct
       | ACoq_tFloat x -> evm, Constr.mkFloat (D.unquote_float64 x)
       | ACoq_tArray (u, arr, def, ty) ->
           let evm, u = D.unquote_universe_level evm u in
-          let evm, arr = Array.fold_left_map (fun evm a -> aux env evm a) evm arr in
+          let evm, arr = ArrayCompat.fold_left_map (fun evm a -> aux env evm a) evm arr in
           let evm, def = aux env evm def in
           let evm, ty = aux env evm ty in
           evm, Constr.mkArray (Univ.Instance.of_array [|u|], arr, def, ty)
diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
index 9dbd3018a..2eadb282c 100644
--- a/template-coq/src/quoter.ml
+++ b/template-coq/src/quoter.ml
@@ -342,7 +342,7 @@ struct
         let u = match Univ.Instance.to_array u with [| u |] -> u | _ -> assert false in
         let def', acc = quote_term acc env sigma def in
         let ty', acc = quote_term acc env sigma ty in
-        let acc, arr' = Array.fold_left_map (fun acc t -> let t', acc = quote_term acc env sigma t in acc, t') acc ar in
+        let acc, arr' = ArrayCompat.fold_left_map (fun acc t -> let t', acc = quote_term acc env sigma t in acc, t') acc ar in
         Q.mkArray (Q.quote_univ_level u) arr' ~default:def' ~ty:ty', acc
       in
       aux acc env trm
diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml
index 50ec20253..47ee0da67 100644
--- a/template-coq/src/tm_util.ml
+++ b/template-coq/src/tm_util.ml
@@ -314,3 +314,20 @@ type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive
   | ACoq_tFloat of 'float64
   | ACoq_tArray of 'universe_level * 'term array * 'term * 'term
 
+module ArrayCompat = struct
+  (** For compat with OCaml < 4.13, copied from https://github.com/ocaml/ocaml/blob/d5b5c34971ed4291c385852f820554ad57adba84/stdlib/array.ml#L195-L207 *)
+  let fold_left_map f acc input_array =
+    let open Array in
+    let len = length input_array in
+    if len = 0 then (acc, [||]) else begin
+      let acc, elt = f acc (unsafe_get input_array 0) in
+      let output_array = make len elt in
+      let acc = ref acc in
+      for i = 1 to len - 1 do
+        let acc', elt = f !acc (unsafe_get input_array i) in
+        acc := acc';
+        unsafe_set output_array i elt;
+      done;
+      !acc, output_array
+    end
+end

From 9332f054d1a0d930e445d3a0973b2dfebf3d116d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 25 Jan 2024 16:17:25 +0100
Subject: [PATCH 3/6] Fix remaining warnings, minor fixups

---
 common/theories/EnvironmentTyping.v          | 4 ++--
 erasure/theories/EEtaExpandedFix.v           | 1 +
 erasure/theories/Typed/OptimizeCorrectness.v | 4 ++--
 pcuic/theories/PCUICEtaExpand.v              | 2 ++
 pcuic/theories/PCUICNormal.v                 | 5 -----
 pcuic/theories/PCUICReduction.v              | 2 ++
 {safechecker => safechecker-plugin}/demo.v   | 2 +-
 safechecker/theories/Loader.v                | 4 ----
 safechecker/theories/PCUICSafeConversion.v   | 3 +--
 utils/theories/wGraph.v                      | 2 ++
 10 files changed, 13 insertions(+), 16 deletions(-)
 rename {safechecker => safechecker-plugin}/demo.v (72%)
 delete mode 100644 safechecker/theories/Loader.v

diff --git a/common/theories/EnvironmentTyping.v b/common/theories/EnvironmentTyping.v
index 8e7f8757b..ff7df2e95 100644
--- a/common/theories/EnvironmentTyping.v
+++ b/common/theories/EnvironmentTyping.v
@@ -1012,12 +1012,12 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E).
 
   Notation lift_sorting_size csize ssize := (lift_sorting_size_gen csize ssize 1).
   Notation typing_sort_size typing_size := (fun t s (tu: typing_sort _ t s) => typing_size t (tSort s) tu).
-  Notation lift_typing_size typing_size := (lift_sorting_size_gen typing_size (typing_sort_size typing_size) 0).
+  Notation lift_typing_size typing_size := (lift_sorting_size_gen typing_size%function (typing_sort_size typing_size%function) 0).
   Notation typing_sort_size1 typing_size := (fun Γ t s (tu: typing_sort1 _ Γ t s) => typing_size Γ t (tSort s) tu).
   Notation on_def_type_sorting_size ssize := (on_def_type_size_gen ssize 1).
   Notation on_def_type_size typing_size := (on_def_type_size_gen (typing_sort_size1 typing_size) 0).
   Notation on_def_body_sorting_size csize ssize := (on_def_body_size_gen csize ssize 1).
-  Notation on_def_body_size typing_size := (on_def_body_size_gen typing_size (typing_sort_size1 typing_size) 0).
+  Notation on_def_body_size typing_size := (on_def_body_size_gen typing_size%function (typing_sort_size1 typing_size%function) 0).
   (* Will probably not pass the guard checker if in a list, must be unrolled like in on_def_* *)
 
   Lemma lift_sorting_size_impl {checking sorting Qc Qs j} csize ssize :
diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
index ccd82e884..9d5eeafb6 100644
--- a/erasure/theories/EEtaExpandedFix.v
+++ b/erasure/theories/EEtaExpandedFix.v
@@ -176,6 +176,7 @@ Inductive expanded_global_declarations : forall (Σ : global_declarations), Prop
 | expanded_global_nil : expanded_global_declarations []
 | expanded_global_cons decl Σ : expanded_global_declarations Σ ->
   expanded_decl Σ decl.2 -> expanded_global_declarations (decl :: Σ).
+Derive Signature for expanded_global_declarations.
 
 Definition expanded_global_env := expanded_global_declarations.
 
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index 201b4a68d..f771c1f06 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -19,6 +19,7 @@ From MetaCoq.Utils Require Import MCList.
 From MetaCoq.Utils Require Import MCPrelude.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Utils Require Import All_Forall.
+Require ssreflect.
 
 Import ExAst.
 Import Kernames.
@@ -2639,8 +2640,7 @@ Proof.
       eapply IHl in hn; tea. now rewrite Nat.add_succ_r in hn.
 Qed.
 
-
-Require Import ssreflect.
+Import ssreflect.
 
 Lemma forallbi_Alli {A} (f : nat -> A -> bool) n l :
   Alli f n l <~> forallbi f n l.
diff --git a/pcuic/theories/PCUICEtaExpand.v b/pcuic/theories/PCUICEtaExpand.v
index 88f900379..f0b4fcecb 100644
--- a/pcuic/theories/PCUICEtaExpand.v
+++ b/pcuic/theories/PCUICEtaExpand.v
@@ -705,6 +705,8 @@ Module Red1Apps.
 
   where " Σ ;;; Γ |- t ⇝ u " := (red1 Σ Γ t u).
 
+  Derive Signature for red1.
+
   Lemma red1_ind_all :
     forall (Σ : global_env) (P : context -> term -> term -> Type),
 
diff --git a/pcuic/theories/PCUICNormal.v b/pcuic/theories/PCUICNormal.v
index 45b8d09bd..96a812230 100644
--- a/pcuic/theories/PCUICNormal.v
+++ b/pcuic/theories/PCUICNormal.v
@@ -317,8 +317,6 @@ Proof.
   - inv whn; solve_discr; easy.
 Qed.
 
-Set Firstorder Solver auto with core.
-
 Definition whnf_whne_dec flags Σ Γ t :
   ({∥whnf flags Σ Γ t∥} + {~∥whnf flags Σ  Γ t∥}) *
   ({∥whne flags Σ Γ t∥} + {~∥whne flags Σ Γ t∥}).
@@ -1936,6 +1934,3 @@ Section Normal.
   Qed.
 
 End Normal.
-
-
-
diff --git a/pcuic/theories/PCUICReduction.v b/pcuic/theories/PCUICReduction.v
index 8a0f0ee6b..b73119528 100644
--- a/pcuic/theories/PCUICReduction.v
+++ b/pcuic/theories/PCUICReduction.v
@@ -153,6 +153,8 @@ Inductive red1 (Σ : global_env) (Γ : context) : term -> term -> Type :=
 
 where " Σ ;;; Γ |- t ⇝ u " := (red1 Σ Γ t u).
 
+Derive Signature for red1.
+
 Definition red1_ctx Σ := (OnOne2_local_env (fun Δ => on_one_decl (fun t t' => red1 Σ Δ t t'))).
 Definition red1_ctx_rel Σ Γ := (OnOne2_local_env (fun Δ => on_one_decl (fun t t' => red1 Σ (Γ ,,, Δ) t t'))).
 
diff --git a/safechecker/demo.v b/safechecker-plugin/demo.v
similarity index 72%
rename from safechecker/demo.v
rename to safechecker-plugin/demo.v
index c784ac360..c52c36837 100644
--- a/safechecker/demo.v
+++ b/safechecker-plugin/demo.v
@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-Require Import MetaCoq.SafeChecker.Loader.
+Require Import MetaCoq.SafeCheckerPlugin.Loader.
 
 MetaCoq SafeCheck (3 + 9).
 
diff --git a/safechecker/theories/Loader.v b/safechecker/theories/Loader.v
deleted file mode 100644
index 8695768af..000000000
--- a/safechecker/theories/Loader.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* Distributed under the terms of the MIT license. *)
-From MetaCoq.Common Require ExtractableLoader.
-
-Declare ML Module "coq-metacoq-safechecker.plugin".
diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v
index b72f18a2c..674002260 100644
--- a/safechecker/theories/PCUICSafeConversion.v
+++ b/safechecker/theories/PCUICSafeConversion.v
@@ -6045,8 +6045,6 @@ Qed.
     _isconv Fallback Γ t1 π1 h1 t2 π2 h2 aux :=
       λ { | leq | hx | r1 | r2 | hd := _isconv_fallback Γ leq t1 π1 h1 t2 π2 h2 r1 r2 hd hx aux }.
 
-  Derive Signature for dlexmod.
-
   Lemma welltyped_R_zipc Σ (wfΣ : abstract_env_ext_rel X Σ) Γ :
     forall x y : pack Γ, welltyped Σ Γ (zipc (tm1 x) (stk1 x)) -> R Γ y x -> welltyped Σ Γ (zipc (tm1 y) (stk1 y)).
   Proof using Type.
@@ -6055,6 +6053,7 @@ Qed.
     pose proof (hΣ := hΣ _ wfΣ). cbn.
     sq.
     destruct x, y; cbn in *.
+    red in HR. cbn in HR. red in HR. cbn in HR.
     depind HR.
     - cbn in *. specialize_Σ wfΣ.
       eapply cored'_postpone in H as [u' [cor eq]].
diff --git a/utils/theories/wGraph.v b/utils/theories/wGraph.v
index 3aec3246c..37318169c 100644
--- a/utils/theories/wGraph.v
+++ b/utils/theories/wGraph.v
@@ -6,6 +6,8 @@ From Equations Require Import Equations.
 
 Local Open Scope Z_scope.
 
+Ltac Tauto.intuition_solver ::= auto with *.
+
 Lemma fold_max_In n m l (H : fold_left Z.max l n = m)
   : n = m \/ In m l.
 Proof.

From 66e14a0506d88492925b218de937bdab60a148de Mon Sep 17 00:00:00 2001
From: nicolas tabareau <nicolas.tabareau@gmail.com>
Date: Fri, 26 Jan 2024 10:41:59 +0100
Subject: [PATCH 4/6] strengthen principal_type_ind

---
 pcuic/theories/PCUICPrincipality.v | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/pcuic/theories/PCUICPrincipality.v b/pcuic/theories/PCUICPrincipality.v
index 4f3da8802..81654c126 100644
--- a/pcuic/theories/PCUICPrincipality.v
+++ b/pcuic/theories/PCUICPrincipality.v
@@ -358,13 +358,14 @@ Section Principality.
 
 End Principality.
 
-Lemma principal_type_ind {cf:checker_flags} {Σ Γ c ind u u' args args'} {wfΣ: wf_ext Σ} :
+Lemma principal_type_ind {cf:checker_flags} {Σ Γ c ind ind' u u' args args'} {wfΣ: wf_ext Σ} :
   Σ ;;; Γ |- c : mkApps (tInd ind u) args ->
-  Σ ;;; Γ |- c : mkApps (tInd ind u') args' ->
+  Σ ;;; Γ |- c : mkApps (tInd ind' u') args' ->
   (∑ ui',
     cmp_ind_universes Σ ind #|args| ui' u *
-    cmp_ind_universes Σ ind #|args'| ui' u') *
-  ws_cumul_pb_terms Σ Γ args args'.
+    cmp_ind_universes Σ ind' #|args'| ui' u') *
+  ws_cumul_pb_terms Σ Γ args args' * 
+  (ind = ind').
 Proof.
   intros h h'.
   destruct (common_typing _ wfΣ h h') as [C [l [r ty]]].
@@ -374,11 +375,9 @@ Proof.
   eapply invert_red_mkApps_tInd in redl as [args'' [-> eq0]]; auto.
   eapply invert_red_mkApps_tInd in redr as [args''' [eqnf eq1]]; auto.
   solve_discr.
-  split.
+  repeat split; eauto. 
   assert (#|args| = #|args'|).
   now rewrite -(All2_length eqargs) -(All2_length eqargs') (All2_length a) (All2_length a0).
-  exists ui'. split; auto.
-
   transitivity l'. now symmetry.
   transitivity args'' => //. now apply red_terms_ws_cumul_pb_terms.
   transitivity l''. symmetry. auto using red_terms_ws_cumul_pb_terms.
@@ -647,7 +646,7 @@ Proof.
       eapply eq_context_upto_inst_case_context => //.
       eapply All2_app. 2:constructor; pcuic.
       specialize (X3 _ _ scrut_ty (eq_term_empty_leq_term X10)).
-      unshelve epose proof (principal_type_ind scrut_ty X3) as [_ indconv]; tea.
+      unshelve epose proof (principal_type_ind scrut_ty X3) as [[_ indconv] _]; tea.
       split; auto.
       eapply All2_app_inv in indconv as [convpars convinds] => //.
       exact (All2_length eqpars).
@@ -658,7 +657,7 @@ Proof.
     specialize (X3 _ _ a0 (eq_term_empty_leq_term X4)).
     eapply eq_term_empty_eq_term in X4.
     assert (wf_ext Σ) by (split; assumption).
-    pose proof (principal_type_ind X3 a0) as [Ruu' X3'].
+    pose proof (principal_type_ind X3 a0) as [[Ruu' X3'] _].
     eapply (type_ws_cumul_pb (pb:=Conv)).
     * clear a0.
       econstructor; eauto.

From 807fc508553158b8ed831fa748f57d0c63b391c7 Mon Sep 17 00:00:00 2001
From: nicolas tabareau <nicolas.tabareau@gmail.com>
Date: Fri, 26 Jan 2024 10:42:43 +0100
Subject: [PATCH 5/6] verified_erasure_pipeline_lookup_env_in for all decls

---
 erasure-plugin/theories/ErasureCorrectness.v | 55 +++++++++++---------
 1 file changed, 31 insertions(+), 24 deletions(-)

diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v
index 9d2f538a6..fbeac012c 100644
--- a/erasure-plugin/theories/ErasureCorrectness.v
+++ b/erasure-plugin/theories/ErasureCorrectness.v
@@ -292,17 +292,27 @@ Section PCUICProof.
     lookup_env Σ kn = Some (PCUICAst.PCUICEnvironment.InductiveDecl decl') ->
     decl = erase_mutual_inductive_body decl').
 
+  Definition erase_decl_equal cmp decl decl' :=
+    match decl, decl' with 
+        EAst.InductiveDecl decl , InductiveDecl decl' => decl = cmp decl'
+      | EAst.ConstantDecl _ , ConstantDecl _ => True
+      | _ , _ => False 
+    end. 
+
   Lemma lookup_env_in_erase_global_deps X_type X deps decls kn normalization_in prf decl :
     EnvMap.EnvMap.fresh_globals decls ->
-    EGlobalEnv.lookup_env (erase_global_deps X_type deps X decls normalization_in prf).1 kn = Some (EAst.InductiveDecl decl) ->
-    exists decl', lookup_global decls kn = Some (InductiveDecl decl') /\ decl = erase_mutual_inductive_body decl'.
+    EGlobalEnv.lookup_env (erase_global_deps X_type deps X decls normalization_in prf).1 kn = Some decl ->
+    exists decl', lookup_global decls kn = Some decl' /\ 
+                  erase_decl_equal erase_mutual_inductive_body decl decl'.
   Proof.
     induction decls in deps, X, normalization_in, prf |- *; cbn [erase_global_deps] => //.
     destruct a => //. destruct g => //.
     - case: (knset_mem_spec k deps) => // hdeps.
       cbn [EGlobalEnv.lookup_env fst lookup_env lookup_global].
       { destruct (eqb_spec kn k) => //.
-        intros hl. eapply IHdecls. now depelim hl. }
+        intro hl; depelim hl; cbn. intro e; noconf e.  
+        eexists; split; eauto. cbn; eauto.    
+        intros hl. cbn. eapply IHdecls. now depelim hl. }
       { intros hl. depelim hl.
         intros hl'.
         eapply IHdecls in hl. destruct hl.
@@ -311,12 +321,12 @@ Section PCUICProof.
         destruct (eqb_spec kn k) => //. subst k.
         destruct H0.
         now eapply PCUICWeakeningEnv.lookup_global_Some_fresh in H0.
-        exact hl'. }
+        exact hl'. } 
     - intros hf; depelim hf.
       case: (knset_mem_spec k deps) => // hdeps.
       cbn [EGlobalEnv.lookup_env fst lookup_env lookup_global].
-      { destruct (eqb_spec kn k) => //.
-        intros hl. noconf hl. subst k. eexists; split; cbn; eauto.
+      { destruct (eqb_spec kn k) => //; cbn.
+        intros hl. noconf hl. subst k. eexists; split; cbn; eauto. cbn; eauto.  
         intros hl'. eapply IHdecls => //. tea. }
       { intros hl'. eapply IHdecls in hf; tea. destruct hf.
         exists x.
@@ -1663,15 +1673,15 @@ Section pipeline_theorem.
   Import PCUICWfEnv.
 
   Lemma verified_erasure_pipeline_lookup_env_in kn decl (efl := EInlineProjections.switch_no_params all_env_flags)  {has_rel : has_tRel} {has_box : has_tBox}  :
-    EGlobalEnv.lookup_env Σ_v kn = Some (EAst.InductiveDecl decl) ->
+    EGlobalEnv.lookup_env Σ_t kn = Some decl ->
     exists decl',
       PCUICAst.PCUICEnvironment.lookup_global (PCUICExpandLets.trans_global_decls
-      (PCUICAst.PCUICEnvironment.declarations
-         Σ.1)) kn = Some (PCUICAst.PCUICEnvironment.InductiveDecl decl')
-       /\ decl = ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl').
+      (PCUICAst.PCUICEnvironment.declarations Σ.1)) kn = Some decl'
+      /\  erase_decl_equal (fun decl => ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl))
+             decl decl'.
   Proof.
     Opaque compose.
-    unfold Σ_v, verified_erasure_pipeline.
+    unfold Σ_t, verified_erasure_pipeline.
     repeat rewrite -transform_compose_assoc.
     destruct_compose; intro. cbn.
     destruct_compose; intro. cbn.
@@ -1713,21 +1723,18 @@ Section pipeline_theorem.
     intro.
     set (EAstUtils.term_global_deps _).
     set (build_wf_env_from_env _ _).
-    epose proof
-      (lookup_env_in_erase_global_deps optimized_abstract_env_impl w t0
-      _ kn _ Hyp0).
     set (EGlobalEnv.lookup_env _ _).
     case_eq o. 2: { intros ?. inversion 1. }
-    destruct g3; intro Ho; [inversion 1|].
-    cbn. inversion 1.
-    specialize (H8 m). forward H8.
-    epose proof (wf_fresh_globals _ HΣ). clear - H10.
-    revert H10. cbn. set (Σ.1). induction 1; econstructor; eauto.
-    cbn. clear -H. induction H; econstructor; eauto.
-    unfold o in Ho; rewrite Ho in H8.
-    specialize (H8 eq_refl).
-    destruct H8 as [decl' [? ?]]. exists decl'; split ; eauto.
-    rewrite <- H10. now destruct decl, m.
+    intros decl' Heq.
+    unshelve epose proof
+      (Hlookup := lookup_env_in_erase_global_deps optimized_abstract_env_impl w t0
+      _ kn _ Hyp0 decl' _ Heq).
+    { epose proof (wf_fresh_globals _ HΣ). clear - H8.
+      revert H8. cbn. set (Σ.1). induction 1; econstructor; eauto.
+      cbn. clear -H. induction H; econstructor; eauto. }
+    destruct Hlookup as [decl'' [? ?]]. exists decl''; split ; eauto.
+    cbn in H10. inversion H10. 
+    now destruct decl' , decl''.
   Qed.
 
   Lemma verified_erasure_pipeline_firstorder_evalue_block :

From 6d8ea79d6a7f299481a6f60dc128ec53a0bd1ada Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 26 Jan 2024 15:27:21 +0100
Subject: [PATCH 6/6] Fix 8.18 warnings and deprecations

---
 common/theories/BasicAst.v                    |  6 ++---
 common/theories/Environment.v                 |  2 ++
 common/theories/EnvironmentReflect.v          |  2 ++
 common/theories/uGraph.v                      | 10 ++++---
 coq.dev                                       |  1 +
 erasure/theories/EArities.v                   |  2 +-
 erasure/theories/EWcbvEvalNamed.v             |  2 +-
 erasure/theories/ErasureFunction.v            |  4 +--
 erasure/theories/ErasureFunctionProperties.v  | 18 ++++++-------
 erasure/theories/Typed/CertifyingBeta.v       |  3 ++-
 erasure/theories/Typed/CertifyingEta.v        |  3 ++-
 erasure/theories/Typed/CertifyingInlining.v   |  3 ++-
 .../theories/Typed/ExtractionCorrectness.v    |  2 +-
 erasure/theories/Typed/OptimizeCorrectness.v  |  4 +--
 erasure/theories/Typed/TypeAnnotations.v      |  2 +-
 .../theories/Typing/PCUICWeakeningConfigTyp.v |  2 +-
 .../theories/ToPCUIC/PCUIC/PCUICTyping.v      |  2 +-
 .../theories/ToTemplate/Template/Typing.v     |  2 +-
 template-coq/src/ast_denoter.ml               |  3 ---
 template-coq/src/constr_denoter.ml            |  2 +-
 template-coq/src/quoter.ml                    |  8 +++---
 template-coq/src/run_template_monad.ml        | 26 +++++++++----------
 template-coq/src/template_monad.ml            |  2 +-
 utils/theories/All_Forall.v                   |  6 ++---
 24 files changed, 62 insertions(+), 55 deletions(-)
 create mode 160000 coq.dev

diff --git a/common/theories/BasicAst.v b/common/theories/BasicAst.v
index f364e0d79..b3908a723 100644
--- a/common/theories/BasicAst.v
+++ b/common/theories/BasicAst.v
@@ -245,9 +245,9 @@ Notation TermoptTyp tm typ := (Judge tm typ None).
 Notation TypUniv ty u := (Judge None ty (Some u)).
 Notation TermTypUniv tm ty u := (Judge (Some tm) ty (Some u)).
 
-Notation j_vass na ty := (Typ ty (* na.(binder_relevance) *)).
-Notation j_vass_s na ty s := (TypUniv ty s (* na.(binder_relevance) *)).
-Notation j_vdef na b ty := (TermTyp b ty (* na.(binder_relevance) *)).
+Notation j_vass na ty := (Typ ty (* na.(binder_relevance) *)) (only parsing).
+Notation j_vass_s na ty s := (TypUniv ty s (* na.(binder_relevance) *)) (only parsing).
+Notation j_vdef na b ty := (TermTyp b ty (* na.(binder_relevance) *)) (only parsing).
 Notation j_decl d := (TermoptTyp (decl_body d) (decl_type d) (* (decl_name d).(binder_relevance) *)).
 Notation j_decl_s d s := (Judge (decl_body d) (decl_type d) s (* (decl_name d).(binder_relevance) *)).
 
diff --git a/common/theories/Environment.v b/common/theories/Environment.v
index bd47913f8..39ba20596 100644
--- a/common/theories/Environment.v
+++ b/common/theories/Environment.v
@@ -4,6 +4,8 @@ From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes.
 From Equations.Prop Require Import Classes EqDecInstances.
 
+Ltac Tauto.intuition_solver ::= auto with *.
+
 Module Type Term.
 
   Parameter Inline term : Type.
diff --git a/common/theories/EnvironmentReflect.v b/common/theories/EnvironmentReflect.v
index 10ea249c3..652647beb 100644
--- a/common/theories/EnvironmentReflect.v
+++ b/common/theories/EnvironmentReflect.v
@@ -4,6 +4,8 @@ From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes Environment Reflect.
 From Equations.Prop Require Import Classes EqDecInstances.
 
+Ltac Tauto.intuition_solver ::= auto with *.
+
 Module EnvironmentReflect (T : Term) (Import E : EnvironmentSig T) (Import TDec : TermDecide T) (Import EDec : EnvironmentDecide T E).
 
   Local Notation extendsb_decls_part Σ Σ'
diff --git a/common/theories/uGraph.v b/common/theories/uGraph.v
index 820419d1d..4a039a202 100644
--- a/common/theories/uGraph.v
+++ b/common/theories/uGraph.v
@@ -2144,28 +2144,30 @@ Section CheckLeq2.
     contradiction HG.
   Defined.
 
-  Let Huctx': global_gc_uctx_invariants uctx'.
+  #[clearbody] Let Huctx' : global_gc_uctx_invariants uctx'.
     unfold uctx'; cbn.
     eapply gc_of_uctx_invariants; tea.
     unfold is_graph_of_uctx, gc_of_uctx in *. cbn.
     destruct (gc_of_constraints uctx.2) as [ctrs|].
     reflexivity. contradiction HG.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let HC' : gc_consistent uctx'.2.
     unfold uctx'; cbn. clear Huctx'.
     apply gc_consistent_iff in HC.
     unfold is_graph_of_uctx, gc_of_uctx in *.
     destruct (gc_of_constraints uctx.2) as [ctrs|].
     exact HC. contradiction HG.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let HG' : Equal_graph G (make_graph uctx').
     unfold uctx' in *; cbn. clear Huctx'.
     unfold is_graph_of_uctx, gc_of_uctx in *.
     destruct (gc_of_constraints uctx.2) as [ctrs|].
     symmetry; exact HG. contradiction HG.
-  Qed.
+  Defined.
 
   Let level_declared (l : Level.t) := LevelSet.In l uctx.1.
 
diff --git a/coq.dev b/coq.dev
new file mode 160000
index 000000000..4335e489b
--- /dev/null
+++ b/coq.dev
@@ -0,0 +1 @@
+Subproject commit 4335e489b977f82a26a74b3542844744dd3470b1
diff --git a/erasure/theories/EArities.v b/erasure/theories/EArities.v
index f167c829a..f80d881f6 100644
--- a/erasure/theories/EArities.v
+++ b/erasure/theories/EArities.v
@@ -835,7 +835,7 @@ Proof.
   rewrite oib.(ind_arity_eq).
   rewrite /isPropositionalArity !destArity_it_mkProd_or_LetIn /=.
   destruct (Sort.is_propositional (ind_sort x0)) eqn:isp; auto.
-  elimtype False; eapply ise.
+  exfalso; eapply ise.
   red. eexists; intuition eauto. right.
   unfold type_of_constructor in e, X.
   destruct s as [indctors [nthcs onc]].
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index 48d2a598a..bb6a357b2 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -1976,7 +1976,7 @@ Proof.
                        lazymatch B with context[x] => idtac | context[z] => idtac end;
                        pose proof (pair H H'); clear H H'
                   end.
-           revert dependent x; intros x H'; exact H'. }
+           generalize dependent x; intros x H'; exact H'. }
        assert ({ vs & All3 (fun v x z => ⊩ v ~ z × eval Σ' E x v) vs args0 args'}) as [vs Hvs]. { let X := match goal with H : All2 _ ?x ?y |- context[All3 _ _ ?x ?y] => H end in
          clear - X; induction X. eexists; econstructor. repeat (destruct_head'_sigT; destruct_head'_prod).
          eexists (_ :: _). econstructor; eauto.
diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v
index 7eb6479be..975f0c373 100644
--- a/erasure/theories/ErasureFunction.v
+++ b/erasure/theories/ErasureFunction.v
@@ -338,7 +338,7 @@ Proof.
 
     + intros hl.
       case: (knset_mem_spec kn0 _) => hin.
-      * elimtype False.
+      * exfalso.
         eapply lookup_global_deps in hl; tea.
         now eapply fresh_global_In in H1.
       * case: (knset_mem_spec kn0 _).
@@ -668,7 +668,7 @@ Proof.
     * rewrite global_deps_union KernameSet.union_spec.
       intros [] fr.
     ** depelim fr. now eapply IHΣ.
-    ** depelim fr. elimtype False. eapply IHΣ in H1; eauto.
+    ** depelim fr. exfalso. eapply IHΣ in H1; eauto.
       destruct d as [[[]]|] eqn:eqd; cbn in H.
       + cbn in H1. eapply (term_global_deps_fresh Σ) in H1; tea. cbn in H2.
         eapply (Forall_map (fun x => x <> kn) fst) in fr.
diff --git a/erasure/theories/ErasureFunctionProperties.v b/erasure/theories/ErasureFunctionProperties.v
index a411fdeb6..24da79c69 100644
--- a/erasure/theories/ErasureFunctionProperties.v
+++ b/erasure/theories/ErasureFunctionProperties.v
@@ -230,7 +230,7 @@ Proof.
     pose proof (wf' := wf.1).
     specialize (H1 kn). forward H1.
     now rewrite KernameSet.singleton_spec. red in H1. destruct H1.
-    elimtype False. destruct H1 as [cst [declc _]].
+    exfalso. destruct H1 as [cst [declc _]].
     { destruct x1 as [d _].
       unshelve eapply declared_minductive_to_gen in d; eauto.
       unshelve eapply declared_constant_to_gen in declc; eauto.
@@ -261,7 +261,7 @@ Proof.
     pose proof (wf' := wf.1).
     specialize (H0 (inductive_mind p.(proj_ind))). forward H0.
     now rewrite KernameSet.singleton_spec. red in H0. destruct H0.
-    elimtype False. destruct H0 as [cst [declc _]].
+    exfalso. destruct H0 as [cst [declc _]].
     {
       unshelve eapply declared_constant_to_gen in declc; eauto.
       red in declc. destruct d as [[[d _] _] _].
@@ -503,7 +503,7 @@ Lemma erase_global_includes X_type (X:X_type.π1) deps decls {normalization_in}
   includes_deps Σ (fst Σ') deps'.
 Proof.
   intros ? sub Σ wfΣ; cbn. induction decls in X, H, sub, prf, deps, deps', Σ , wfΣ, normalization_in |- *.
-  - simpl. intros i hin. elimtype False.
+  - simpl. intros i hin. exfalso.
     edestruct (H i hin) as [[decl Hdecl]]; eauto.
     rewrite /lookup_env (prf _ wfΣ) in Hdecl. noconf Hdecl.
   - intros i hin.
@@ -976,7 +976,7 @@ Proof.
     ++ intros kn'deps kn'eg'.
       eapply in_erase_global_deps_acc in kn'eg'.
       destruct kn'eg'. eapply KernameSet.mem_spec in H. congruence.
-      elimtype False. clear -prf wfΣ H.
+      exfalso. clear -prf wfΣ H.
       specialize (prf _ wfΣ).
       pose proof (abstract_env_wf _ wfΣ) as []. eapply wf_fresh_globals in X0.
       rewrite prf in X0. depelim X0.
@@ -991,7 +991,7 @@ Proof.
       ++ intros kn'deps kn'eg'.
         eapply in_erase_global_deps_acc in kn'eg'.
         destruct kn'eg'. eapply KernameSet.mem_spec in H. congruence.
-        elimtype False. clear -prf wfΣ H.
+        exfalso. clear -prf wfΣ H.
         specialize (prf _ wfΣ).
         pose proof (abstract_env_wf _ wfΣ) as []. eapply wf_fresh_globals in X0.
         rewrite prf in X0. depelim X0.
@@ -1142,7 +1142,7 @@ Proof.
           now eapply in_global_deps.
       * intros hwf.
         case: (knset_mem_spec kn _); intros hin.
-        ** elimtype False.
+        ** exfalso.
             depelim hwf.
             eapply in_global_deps_fresh in hin => //.
         ** depelim hwf. rewrite -IHΣ => //.
@@ -1158,7 +1158,7 @@ Proof.
             now eapply in_global_deps.
       ** intros hwf.
         case: (knset_mem_spec kn _); intros hin.
-        *** elimtype False.
+        *** exfalso.
             eapply in_global_deps_fresh in hin => //.
         *** rewrite -IHΣ => //.
     + intros wf; depelim wf.
@@ -1176,7 +1176,7 @@ Proof.
             now eapply in_global_deps.
       ** intros hwf.
         case: (knset_mem_spec kn _); intros hin.
-        *** elimtype False.
+        *** exfalso.
             eapply in_global_deps_fresh in hin => //.
         *** rewrite -IHΣ => //.
 Qed.
@@ -2007,7 +2007,7 @@ Proof.
   destruct (inspect_bool (is_erasableb X_type Xext [] t wt)) eqn:heq.
   - simp erase. rewrite heq.
     simp erase => //.
-  - elimtype False.
+  - exfalso.
     pose proof (abstract_env_exists X) as [[? wf]].
     destruct (@is_erasableP X_type Xext _ [] t wt) => //. apply n.
     intros. sq. now rewrite (abstract_env_ext_irr _ H H2).
diff --git a/erasure/theories/Typed/CertifyingBeta.v b/erasure/theories/Typed/CertifyingBeta.v
index b41a3f628..c5aac5a25 100644
--- a/erasure/theories/Typed/CertifyingBeta.v
+++ b/erasure/theories/Typed/CertifyingBeta.v
@@ -74,7 +74,7 @@ Definition betared_def {A}
 
 Definition template_betared : TemplateTransform :=
   fun Σ => Ok (timed "Inlining" (fun _ => mk_global_env (universes Σ) (betared_globals (declarations Σ)) (retroknowledge Σ))).
-
+(*
 Module Ex1.
 
   Definition foo (n : nat) := (fun x => x) n.
@@ -92,3 +92,4 @@ Module Ex1.
     lookup_env foo_before.1 <%% foo %%> -> False.
   Proof. easy. Qed.
 End Ex1.
+*)
\ No newline at end of file
diff --git a/erasure/theories/Typed/CertifyingEta.v b/erasure/theories/Typed/CertifyingEta.v
index 3f3fb0a82..c1af63705 100644
--- a/erasure/theories/Typed/CertifyingEta.v
+++ b/erasure/theories/Typed/CertifyingEta.v
@@ -253,7 +253,7 @@ Definition template_eta
                                               Σ
                                               seeds
                                               erasure_ignore)).
-
+(*
 Module Examples.
 
   Module Ex1.
@@ -366,3 +366,4 @@ Module Examples.
   End Ex5.
 
 End Examples.
+*)
\ No newline at end of file
diff --git a/erasure/theories/Typed/CertifyingInlining.v b/erasure/theories/Typed/CertifyingInlining.v
index 906dc8b60..b97fc1c27 100644
--- a/erasure/theories/Typed/CertifyingInlining.v
+++ b/erasure/theories/Typed/CertifyingInlining.v
@@ -155,7 +155,7 @@ Definition template_inline (should_inline : kername -> bool) : TemplateTransform
     (fun _ => (mk_global_env (universes Σ)
                              (inline_globals should_inline (declarations Σ))
                              (retroknowledge Σ)))).
-
+(*
 Module Tests.
 
   (** Inlining into the local *)
@@ -225,3 +225,4 @@ Module Tests.
   End Ex6.
 
 End Tests.
+*)
\ No newline at end of file
diff --git a/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v
index 1a9db7311..a7552b0e2 100644
--- a/erasure/theories/Typed/ExtractionCorrectness.v
+++ b/erasure/theories/Typed/ExtractionCorrectness.v
@@ -129,7 +129,7 @@ Proof.
   intros his.
   rewrite erase_equation_1.
   destruct inspect_bool. now cbn.
-  elimtype False.
+  exfalso.
   move/negP: i => hi. apply hi.
   now apply/is_erasableP.
 Qed.
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index 4475b01ff..03b7d4219 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -4244,8 +4244,8 @@ Lemma dearg_branch_body_rec_substl_correct : forall mm args0 t ctx0,
     = substl (List.rev args0) t.
 Proof.
   intros mm args0 t ctx0 Hc Hlen Hctx Hv.
-  revert dependent args0.
-  revert dependent t.
+  generalize dependent args0.
+  generalize dependent t.
   revert ctx0.
   induction mm;simpl;intros ctx0 t Hv args0 Hc Hlen Hctx.
   - unfold complete_ctx_mask;cbn.
diff --git a/erasure/theories/Typed/TypeAnnotations.v b/erasure/theories/Typed/TypeAnnotations.v
index 55c322504..7984f8795 100644
--- a/erasure/theories/Typed/TypeAnnotations.v
+++ b/erasure/theories/Typed/TypeAnnotations.v
@@ -233,7 +233,7 @@ Lemma Forall_mapi :
   Forall P (mapi_rec f l n).
 Proof.
   intros A B n P f l H.
-  revert dependent n.
+  generalize dependent n.
   induction l; intros n.
   - constructor.
   - cbn. inversion H;subst. constructor;auto.
diff --git a/pcuic/theories/Typing/PCUICWeakeningConfigTyp.v b/pcuic/theories/Typing/PCUICWeakeningConfigTyp.v
index 841911e2f..916e2bc95 100644
--- a/pcuic/theories/Typing/PCUICWeakeningConfigTyp.v
+++ b/pcuic/theories/Typing/PCUICWeakeningConfigTyp.v
@@ -95,7 +95,7 @@ Proof.
   all: repeat destruct ?; subst.
   all: lazymatch goal with
        | [ H : ctx_inst _ _ _ _ |- ctx_inst _ _ _ _ ]
-         => revert dependent H;
+         => generalize dependent H;
             repeat match goal with
               | [ |- context[typing_size ?x] ]
                 => generalize (typing_size x); clear x; intro
diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v b/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v
index 6e8d3e747..d03f775ca 100644
--- a/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v
+++ b/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v
@@ -51,7 +51,7 @@ Section quote_typing.
   Proof.
     change (forall Γ t T, ground_quotable (@typing cf Σ Γ t T)) in quote_typing'.
     destruct pf.
-    Time all: [ > try time replace_quotation_of_goal () .. ].
+    all: [ > try replace_quotation_of_goal () .. ].
   Defined.
 End quote_typing.
 #[export] Instance quote_typing {cf Σ Γ t T} : ground_quotable (@typing cf Σ Γ t T) := quote_typing'.
diff --git a/quotation/theories/ToTemplate/Template/Typing.v b/quotation/theories/ToTemplate/Template/Typing.v
index 34283aa43..dc1da98a6 100644
--- a/quotation/theories/ToTemplate/Template/Typing.v
+++ b/quotation/theories/ToTemplate/Template/Typing.v
@@ -64,7 +64,7 @@ Section quote_typing.
     all: change (forall Γ t T, ground_quotable (@typing cf Σ Γ t T)) in quote_typing'.
     all: change (forall Γ t s T, ground_quotable (@typing_spine cf Σ Γ t s T)) in quote_typing_spine'.
     all: destruct pf.
-    Time all: [ > time replace_quotation_of_goal () .. ].
+    all: [ > replace_quotation_of_goal () .. ].
   Defined.
 End quote_typing.
 #[export] Instance quote_typing {cf Σ Γ t T} : ground_quotable (@typing cf Σ Γ t T) := quote_typing'.
diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml
index 9dd801273..0882701c5 100644
--- a/template-coq/src/ast_denoter.ml
+++ b/template-coq/src/ast_denoter.ml
@@ -65,16 +65,13 @@ struct
   let mkEvar = mkEvar
   let mkSort = mkSort
   let mkCast = mkCast
-  let mkConst = mkConst
   let mkProd = mkProd
 
   let mkLambda = mkLambda
   let mkApp = mkApp
   let mkLetIn = mkLetIn
   let mkFix = mkFix
-  let mkConstruct = mkConstruct
   let mkCoFix = mkCoFix
-  let mkInd = mkInd
   let mkCase = mkCase
   let mkProj = mkProj
   let mkInt = mkInt
diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml
index 78f8d8732..48e0e1a48 100644
--- a/template-coq/src/constr_denoter.ml
+++ b/template-coq/src/constr_denoter.ml
@@ -195,7 +195,7 @@ struct
         CErrors.user_err (str "It is not possible to unquote a fresh level in Strict Unquote Universe Mode.")
       else
         let evm, l = Evd.new_univ_level_variable (Evd.UnivFlexible false) evm in
-        debug (fun () -> str"Fresh level " ++ Univ.Level.pr l ++ str" was added to the context.");
+        debug (fun () -> str"Fresh level " ++ Univ.Level.raw_pr l ++ str" was added to the context.");
         evm, l
     else if constr_equall h lzero then
       match args with
diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
index 10773cbff..77e22d080 100644
--- a/template-coq/src/quoter.ml
+++ b/template-coq/src/quoter.ml
@@ -208,8 +208,8 @@ struct
         let cstrs, eqs = UGraph.constraints_of_universes g in
         UGraph.domain g, cstrs, eqs
       | Some l ->
-        debug Pp.(fun () -> str"Quoting graph restricted to: " ++ Univ.Level.Set.pr Univ.Level.pr l);
-        (* Feedback.msg_debug Pp.(str"Graph is: "  ++ UGraph.pr_universes Univ.Level.pr (UGraph.repr g)); *)
+        debug Pp.(fun () -> str"Quoting graph restricted to: " ++ Univ.Level.Set.pr Univ.Level.raw_pr l);
+        (* Feedback.msg_debug Pp.(str"Graph is: "  ++ UGraph.pr_universes Univ.Level.raw_pr (UGraph.repr g)); *)
         let dom = UGraph.domain g in
         let kept = Univ.Level.Set.inter dom l in
         let kept = Univ.Level.Set.remove Univ.Level.set kept in
@@ -227,7 +227,7 @@ struct
         eqs (levels, cstrs)
     in
     let levels = Univ.Level.Set.add Univ.Level.set levels in
-    debug Pp.(fun () -> str"Universe context: " ++ Univ.pr_universe_context_set Univ.Level.pr (levels, cstrs));
+    debug Pp.(fun () -> str"Universe context: " ++ Univ.pr_universe_context_set Univ.Level.raw_pr (levels, cstrs));
     time (Pp.str"Quoting universe context")
       (fun uctx -> Q.quote_univ_contextset uctx) (levels, cstrs)
 
@@ -405,7 +405,7 @@ struct
             List.fold_left (fun (ls,acc) (nm,(ctx, ty),ar) ->
               let ty = Term.it_mkProd_or_LetIn ty ctx in
               let ty = Inductive.abstract_constructor_type_relatively_to_inductive_types_context ntyps t ty in
-              let ctx, concl = Term.decompose_prod_assum ty in
+              let ctx, concl = Term.decompose_prod_decls ty in
               let argctx, parsctx =
                 CList.chop (List.length ctx - List.length mib.mind_params_ctxt) ctx
               in
diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
index 681adb262..1c94b2e27 100644
--- a/template-coq/src/run_template_monad.ml
+++ b/template-coq/src/run_template_monad.ml
@@ -70,12 +70,12 @@ let rec unquote_pos trm : int =
   let (h,args) = app_full trm [] in
   match args with
     [x] ->
-    if constr_equall h cposI then 
+    if constr_equall h cposI then
       (2 * unquote_pos x + 1)
     else if constr_equall h cposO then
       (2 * unquote_pos x)
     else not_supported_verb trm "unquote_pos"
-  | [] -> 
+  | [] ->
     if constr_equall h cposzero then 1
     else not_supported_verb trm "unquote_pos"
   | _ -> bad_term_verb trm "unquote_pos"
@@ -87,7 +87,7 @@ let unquote_Z trm : int =
      if constr_equall h cZpos then unquote_pos x
      else if constr_equall h cZneg then - unquote_pos x
      else not_supported_verb trm "unquote_pos"
-  | [] -> 
+  | [] ->
     if constr_equall h cZ0 then 0
     else not_supported_verb trm "unquote_pos"
   | _ -> bad_term_verb trm "unquote_pos"
@@ -96,12 +96,12 @@ let unquote_constraint_type trm (* of type constraint_type *) : constraint_type
   let (h,args) = app_full trm [] in
   match args with
     [x] ->
-    if constr_equall h tunivLe then 
+    if constr_equall h tunivLe then
       let n = unquote_Z x in
       if n = 0 then Univ.Le
       else Univ.Lt
     else not_supported_verb trm "unquote_constraint_type"
-  | [] -> 
+  | [] ->
     if constr_equall h tunivEq then Univ.Eq
     else not_supported_verb trm "unquote_constraint_type"
   | _ -> bad_term_verb trm "unquote_constraint_type"
@@ -176,7 +176,7 @@ let denote_variance trm (* of type Variance *) : Variance.t =
   else if constr_equall trm cInvariant then Variance.Invariant
   else not_supported_verb trm "denote_variance"
 
-  
+
 let denote_variance evm trm (* of type Variance.t list *) : _ * Variance.t array =
   let variances = List.map denote_variance (unquote_list trm) in
   evm, Array.of_list variances
@@ -243,9 +243,9 @@ let unquote_one_inductive_entry env evm trm (* of type one_inductive_entry *) :
 let map_option f o =
   match o with
   | Some x -> Some (f x)
-  | None -> None          
+  | None -> None
 
-let denote_decl env evm d = 
+let denote_decl env evm d =
   let (h, args) = app_full d [] in
   if constr_equall h tmkdecl then
     match args with
@@ -262,7 +262,7 @@ let denote_decl env evm d =
 
 let denote_context env evm ctx =
   fold_env_evm_right denote_decl env evm (unquote_list ctx)
-  
+
 let unquote_mutual_inductive_entry env evm trm (* of type mutual_inductive_entry *) : _ * _ * Entries.mutual_inductive_entry =
   let (h,args) = app_full trm [] in
   if constr_equall h tBuild_mutual_inductive_entry then
@@ -301,10 +301,10 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool
   let evm' = Evd.from_env env in
   let evm', ctx, mind = unquote_mutual_inductive_entry env evm' mind in
   let () = DeclareUctx.declare_universe_context ~poly:false ctx in
-  let evm, mind = 
+  let evm, mind =
     if infer_univs then
       let ctx, mind = Tm_util.RetypeMindEntry.infer_mentry_univs env evm' mind in
-      debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.pr_universe_context_set (Level.pr) ctx));
+      debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.pr_universe_context_set UnivNames.pr_with_global_universes ctx));
       DeclareUctx.declare_universe_context ~poly:false ctx;
       Evd.merge_context_set Evd.UnivRigid evm ctx, mind
     else evm, mind
@@ -324,7 +324,7 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool
       let ind = (ind_kn, i) in
       let univs = (Entries.Monomorphic_entry, Names.Id.Map.empty) in
       let inhabitant_id = List.hd oie.mind_entry_consnames in
-      let fields, _ = Term.decompose_prod_assum (List.hd oie.mind_entry_lc) in
+      let fields, _ = Term.decompose_prod_decls (List.hd oie.mind_entry_lc) in
       let fieldimpls = List.map (fun _ -> []) fields in
       let pfs = List.map (fun _ -> dflt_pf) fields in
       let projections = Record.Internal.declare_projections ind univs ~kind:Decls.Definition inhabitant_id pfs fieldimpls fields in
@@ -408,7 +408,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
       let param = Declare.ParameterEntry entry in
       let n = Declare.declare_constant ~name ~kind:Decls.(IsDefinition Definition) param in
       let env = Global.env () in
-      k ~st env evm (Constr.mkConst n)
+      k ~st env evm (Constr.mkConstU (n, Univ.Instance.empty))
   | TmAxiomTerm (name,typ) ->
     if intactic
     then not_in_tactic "tmAxiom"
diff --git a/template-coq/src/template_monad.ml b/template-coq/src/template_monad.ml
index da3592251..be094cd3b 100644
--- a/template-coq/src/template_monad.ml
+++ b/template-coq/src/template_monad.ml
@@ -233,7 +233,7 @@ let next_action env evd (pgm : constr) : template_monad * _ =
     with _ ->
       CErrors.user_err (str "Invalid argument or not yet implemented. The argument must be a TemplateProgram: " ++ Printer.pr_constr_env env evd coConstr)
   in
-  let eq_gr t = Names.GlobRef.equal glob_ref (Lazy.force t) in
+  let eq_gr t = Environ.QGlobRef.equal env glob_ref (Lazy.force t) in
   if eq_gr ptmBind || eq_gr ttmBind then
     let () = ppdebug 1 (fun () -> Pp.(str "MetaCoq: TemplateProgram: processing tmBind")) in
     match args with
diff --git a/utils/theories/All_Forall.v b/utils/theories/All_Forall.v
index 1b2cc9abb..cace5b97b 100644
--- a/utils/theories/All_Forall.v
+++ b/utils/theories/All_Forall.v
@@ -1739,7 +1739,7 @@ Qed.
 Lemma Forall3_All3 {A B C} {P : A -> B -> C -> Prop} l l' l'' : Forall3 P l l' l'' -> All3 P l l' l''.
 Proof.
   intros f; induction l in l', l'', f |- *; destruct l', l''; try constructor; auto.
-  1-6: elimtype False; inv f.
+  1-6: exfalso; inv f.
   inv f; auto.
   apply IHl. inv f; auto.
 Qed.
@@ -2748,7 +2748,7 @@ Lemma All2_dep_nth_error {A B} {P : A -> B -> Type} {P' : forall a b, P a b -> T
   (H2 : nth_error l' n = Some t') :
   P' t t' (All2_nth_error n t t' H H1 H2).
 Proof.
-  revert dependent n; induction H'; destruct n; cbn; try congruence.
+  generalize dependent n; induction H'; destruct n; cbn; try congruence.
   { intros H1 H2.
     set (k := f_equal _ H1); clearbody k; cbn in k; clear H1; subst.
     set (k := f_equal _ H2); clearbody k; cbn in k; clear H2; subst.
@@ -2804,7 +2804,7 @@ Lemma Forall2_dep_nth_error {A B} {P : A -> B -> Prop} {P' : forall a b, P a b -
   (H2 : nth_error l' n = Some t') :
   P' t t' (Forall2_nth_error n t t' H H1 H2).
 Proof.
-  revert dependent n; induction H'; destruct n; cbn; try congruence.
+  generalize dependent n; induction H'; destruct n; cbn; try congruence.
   { intros H1 H2.
     set (k := f_equal _ H1); clearbody k; cbn in k; clear H1; subst.
     set (k := f_equal _ H2); clearbody k; cbn in k; clear H2; subst.