Merge pull request #1035 from proux01/coq_18224

Adapt to coq/coq#18224
MetaCoq · Mar 14, 2024 · 3eca445 · 3eca445
2 parents be825a7 + 2814d2a
commit 3eca445
Show file tree

Hide file tree

Showing 10 changed files with 13 additions and 17 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/erasure/theories/Typed/ExtractionCorrectness.v b/erasure/theories/Typed/ExtractionCorrectness.v
@@ -692,7 +692,6 @@ Proof.
     + subst t'' t'.
       rewrite trans_env_remove_match_on_box_env.
       unshelve eapply (EOptimizePropDiscr.remove_match_on_box_correct (fl := default_wcbv_flags)) => //=.
-      { reflexivity. }
       { cbn. now eapply wf_erase_global_decls_recursive. }
       { simpl. eapply EWellformed.wellformed_closed_env.
         now eapply wf_erase_global_decls_recursive. }

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
@@ -45,8 +45,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/translations/MiniHoTT.v b/translations/MiniHoTT.v
@@ -119,8 +119,8 @@ Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Bind Scope fibration_scope with sigT.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
-Notation "x .1" := (pr1 x) (at level 2, left associativity, format "x .1") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 2, left associativity, format "x .2") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 
 Notation compose := (fun g f x => g (f x)).
 Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.

diff --git a/translations/MiniHoTT_paths.v b/translations/MiniHoTT_paths.v
@@ -122,8 +122,8 @@ Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Bind Scope fibration_scope with sigT.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
-Notation "x .1" := (pr1 x) (at level 2, left associativity, format "x .1") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 2, left associativity, format "x .2") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 
 Notation compose := (fun g f x => g (f x)).
 Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.

diff --git a/translations/sigma.v b/translations/sigma.v
@@ -19,8 +19,8 @@ Open Scope sigma_scope.
 Notation "{ x  &&  P }" := (sigma (fun x => P)) : type_scope.
 Notation "{ t : A && P }" := (sigma A (fun t => P)) : type_scope.
 Notation "( x ; y )" := (mk_sig x y) : sigma_scope.
-Notation "x .1" := (π1 x) (at level 2, left associativity, format "x .1") : sigma_scope.
-Notation "x .2" := (π2 x) (at level 2, left associativity, format "x .2") : sigma_scope.
+Notation "x .1" := (π1 x) : sigma_scope.
+Notation "x .2" := (π2 x) : sigma_scope.
 Notation "'∃' x .. y , p" := (sigma _ (fun x => .. (sigma _ (fun y => p)) ..))
   (at level 200, x binder, right associativity,
    format "'[' '∃'  '/  ' x  ..  y ,  '/  ' p ']'")

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