Adapt to coq/coq#18224

MetaCoq · Feb 4, 2024 · 1f7cfd0 · 1f7cfd0
1 parent e6368e3
commit 1f7cfd0
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 10 deletions.
diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
@@ -900,7 +900,7 @@ Lemma transform_wf_global {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
   wf_glob (efl := efl) Σ -> wf_glob (efl := switch_cstr_as_blocks efl) (transform_blocks_env Σ).
 Proof.
   intros hasp cstrbl hasapp hasb hasr etag wfg.
-  unshelve eapply (gen_transform_env_wf (gt := GTExt efl _)) => //. exact hasapp.
+  unshelve eapply (gen_transform_env_wf (gt := GTExt efl _)) => //.
   eapply Pre_glob => //.
 Qed.
 

diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v
@@ -944,7 +944,7 @@ Proof.
       { apply nisa. intros. rewrite (abstract_env_ext_irr _ H wfΣ).
         eapply invert_cumul_arity_r; tea. }
       { destruct s as [Hs].
-        unshelve epose proof (H := unique_sorting_equality_propositional _ wf Hs Hu' p) => //. reflexivity. congruence. }
+        unshelve epose proof (H := unique_sorting_equality_propositional _ wf Hs Hu' p) => //. congruence. }
   Qed.
 
 Equations? is_erasable {X_type X} {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ} (Γ : context) (t : PCUICAst.term)

diff --git a/pcuic/theories/PCUICInductiveInversion.v b/pcuic/theories/PCUICInductiveInversion.v
@@ -1322,7 +1322,6 @@ Proof.
   destruct Σ.
   move: ont. rewrite PCUICOnFreeVars.on_free_vars_mkApps /= => /andP[] // => onn onargs.
   unshelve eapply (red_mkApps_tRel (Γ := exist Γ onΓ) _ hnth db) in red as [args' [eq redargs]] => //.
-  now cbn.
   exists args'; split => //.
   cbn in redargs. solve_all.
   eapply into_closed_red; eauto.

diff --git a/pcuic/theories/PCUICSubstitution.v b/pcuic/theories/PCUICSubstitution.v
@@ -1787,7 +1787,7 @@ Proof.
   unshelve eapply on_wf_global_env_impl ; tea.
   clear. intros * HΣ HP HQ Hty.
   intros. subst Γ.
-  unshelve eapply lift_typing_impl with (1 := Hty _ _ X _) => t T HT.
+  unshelve eapply lift_typing_impl with (1 := Hty _ _ X _) => [||t T HT].
   3: rewrite !subst_inst; eapply HT => //.
   now unshelve eapply subslet_well_subst.
 Qed.

diff --git a/test-suite/hott_example.v b/test-suite/hott_example.v
@@ -46,8 +46,8 @@ Module Hott_Notations.
 Notation "g ∘ f" := (compose g%function f%function) (at level 1): function_scope.
 
 Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
-Notation "x .1" := (projT1 x) (at level 3).
-Notation "x .2" := (projT2 x) (at level 3).
+Notation "x .1" := (projT1 x).
+Notation "x .2" := (projT2 x).
 Notation " ( x ; p ) " := (existT _ x p).
 
 Notation "f == g" := (forall x, f x = g x) (at level 70).

diff --git a/utils/theories/MCProd.v b/utils/theories/MCProd.v
@@ -6,10 +6,8 @@ Local Coercion is_true : bool >-> Sortclass.
 
 Declare Scope pair_scope.
 
-Notation "p .1" := (fst p)
-  (at level 2, left associativity, format "p .1") : pair_scope.
-Notation "p .2" := (snd p)
-  (at level 2, left associativity, format "p .2") : pair_scope.
+Notation "p .1" := (fst p) : pair_scope.
+Notation "p .2" := (snd p) : pair_scope.
 Open Scope pair_scope.
 
 Notation "x × y" := (prod x y ) (at level 80, right associativity).