Merge pull request #27 from Alizter/adapt-to-16004

Adapt w.r.t coq/coq#16004
coq-community · May 11, 2022 · 495d547 · 495d547
2 parents 0d0de67 + cc548ed
commit 495d547
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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")) *)