Fix remaining warnings, minor fixups

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 :

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.
 

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.

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),
 

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.
-
-
-

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'))).
 

safechecker/demo.v → 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).
 

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]].

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.