From cc548ed9f9c126953087acc5a5cda63025b961e8 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 9 May 2022 16:58:14 +0100 Subject: [PATCH] Adapt w.r.t coq/coq#16004 --- theories/Autosubst_Basics.v | 2 +- theories/Autosubst_Derive.v | 14 +++++++------- theories/Autosubst_MMap.v | 14 +++++++------- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/theories/Autosubst_Basics.v b/theories/Autosubst_Basics.v index b7f08af..477c87c 100644 --- a/theories/Autosubst_Basics.v +++ b/theories/Autosubst_Basics.v @@ -139,7 +139,7 @@ Tactic Notation "epose" open_constr(T) := eassert _;[refine T | idtac]. Definition id {A} (x : A) := x. Arguments id {A} x /. -Hint Unfold id : core. +Global Hint Unfold id : core. Ltac fold_id := repeat match goal with diff --git a/theories/Autosubst_Derive.v b/theories/Autosubst_Derive.v index c3dbb8f..297d035 100644 --- a/theories/Autosubst_Derive.v +++ b/theories/Autosubst_Derive.v @@ -14,7 +14,7 @@ Ltac derive_Ids := intro; solve | constructor 15; [app_var] | constructor 16; [app_var] | constructor 17; [app_var] | constructor 18; [app_var] | constructor 19; [app_var] | constructor 20; [app_var]]. -Hint Extern 0 (Ids _) => derive_Ids : derive. +Global Hint Extern 0 (Ids _) => derive_Ids : derive. Ltac derive_Rename := let inst := fresh "dummy" in (* hack/workaround *) @@ -48,7 +48,7 @@ Ltac derive_Rename := let t := map t in exact t end end. -Hint Extern 0 (Rename _) => derive_Rename : derive. +Global Hint Extern 0 (Rename _) => derive_Rename : derive. Ltac has_var s := match s with @@ -104,7 +104,7 @@ Ltac derive_Subst := end end end. -Hint Extern 0 (Subst _) => derive_Subst : derive. +Global Hint Extern 0 (Subst _) => derive_Subst : derive. Ltac derive_HSubst := let inst := fresh "dummy" in (* hack/workaround *) @@ -153,7 +153,7 @@ Ltac derive_HSubst := let t := map t in exact t end end. -Hint Extern 0 (HSubst _ _) => derive_HSubst : derive. +Global Hint Extern 0 (HSubst _ _) => derive_HSubst : derive. Lemma mmap_id_ext {A B} {inst : MMap A B} `{@MMapLemmas A B inst} `{@MMapExt A B inst} (f : A -> A) (b : B) : @@ -379,7 +379,7 @@ Ltac derive_SubstLemmas := constructor; hnf; [apply rename_subst|apply subst_id|reflexivity|apply subst_comp] end. -Hint Extern 0 (SubstLemmas _) => derive_SubstLemmas : derive. +Global Hint Extern 0 (SubstLemmas _) => derive_SubstLemmas : derive. Ltac derive_HSubstLemmas := let ih := fresh "dummy" in (* hack/workaround *) @@ -402,7 +402,7 @@ Ltac derive_HSubstLemmas := constructor; hnf; [exact hsubst_id|reflexivity|exact hsubst_comp] end. -Hint Extern 0 (HSubstLemmas _ _) => derive_HSubstLemmas : derive. +Global Hint Extern 0 (HSubstLemmas _ _) => derive_HSubstLemmas : derive. Ltac derive_SubstHSubstComp := let ih := fresh "dummy" in (* hack/workaround *) @@ -431,7 +431,7 @@ Ltac derive_SubstHSubstComp := rewrite ?up_hcomp, ?up_hcomp_n, ?hcomp_lift_n_internal, ?mmap_comp; try apply mmap_ext; intros; apply ih end. -Hint Extern 0 (SubstHSubstComp _ _) => derive_SubstHSubstComp : derive. +Global Hint Extern 0 (SubstHSubstComp _ _) => derive_SubstHSubstComp : derive. (* Local Variables: *) (* coq-load-path: (("." "Autosubst")) *) diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v index cc4e33e..5d75b28 100644 --- a/theories/Autosubst_MMap.v +++ b/theories/Autosubst_MMap.v @@ -94,12 +94,12 @@ Ltac mmap_typeclass_normalizeH H := let s := constr:(@mmap A B _ f) in progress change (@mmap A B _ f) with s end. -Hint Rewrite @mmap_id_instE @mmap_const_instE : mmap. -Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR +Global Hint Rewrite @mmap_id_instE @mmap_const_instE : mmap. +Global Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR using exact _ : mmap. -Hint Rewrite @mmap_id_instE @mmap_const_instE : autosubst. -Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR +Global Hint Rewrite @mmap_id_instE @mmap_const_instE : autosubst. +Global Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR using exact _ : autosubst. Ltac msimpl := @@ -144,16 +144,16 @@ Ltac derive_MMap := let ys := tmap ys in exact ys end end. -Hint Extern 0 (MMap _ _) => derive_MMap : derive. +Global Hint Extern 0 (MMap _ _) => derive_MMap : derive. Ltac derive_MMapLemmas := constructor; [ let x := fresh in intros x; induction x; simpl; f_equal; trivial; apply mmap_id | let x := fresh in intros ?? x; induction x; simpl; f_equal; trivial; apply mmap_comp ]. -Hint Extern 0 (MMapLemmas _ _) => derive_MMapLemmas : derive. +Global Hint Extern 0 (MMapLemmas _ _) => derive_MMapLemmas : derive. Ltac derive_MMapExt := intros ???; fix FIX 1; let x := fresh in intros x; destruct x; simpl; f_equal; auto using mmap_ext. -Hint Extern 0 (MMapExt _ _) => derive_MMapExt : derive. +Global Hint Extern 0 (MMapExt _ _) => derive_MMapExt : derive. (* Local Variables: *) (* coq-load-path: (("." "Autosubst")) *)