Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt to https://github.com/coq/coq/pull/18224 #1035

Merged
merged 1 commit into from
Mar 14, 2024
Merged

Adapt to https://github.com/coq/coq/pull/18224 #1035

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion erasure/theories/EConstructorsAsBlocks.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
2 changes: 1 addition & 1 deletion erasure/theories/ErasureFunction.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
1 change: 0 additions & 1 deletion erasure/theories/Typed/ExtractionCorrectness.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. }
Expand Down
1 change: 0 additions & 1 deletion pcuic/theories/PCUICInductiveInversion.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion pcuic/theories/PCUICSubstitution.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions test-suite/hott_example.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
4 changes: 2 additions & 2 deletions translations/MiniHoTT.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions translations/MiniHoTT_paths.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions translations/sigma.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ']'")
Expand Down
6 changes: 2 additions & 4 deletions utils/theories/MCProd.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
Loading