Add locality to Hint commands

coq-community · Sep 11, 2023 · 175a5b5 · 175a5b5
1 parent b38f24b
commit 175a5b5
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
@@ -1039,7 +1039,7 @@ Proof.
   destruct k; apply E0_eq_intro; reflexivity. 
 Qed.
 
-Hint Rewrite Canon_Omega : E0_rw.
+#[export] Hint Rewrite Canon_Omega : E0_rw.
 
 Lemma CanonSSn (i:nat) :
   forall alpha n  , alpha <> E0zero ->
@@ -1095,7 +1095,7 @@ Proof.
   simpl;   apply T1limit_canonS_not_zero; auto.
 Qed.
 
-#[global]
+#[export]
   Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.
 
 Lemma CanonS_phi0_Succ alpha i : CanonS (E0phi0 (E0succ alpha)) i =

diff --git a/theories/ordinals/Epsilon0/Hprime.v b/theories/ordinals/Epsilon0/Hprime.v
@@ -94,7 +94,7 @@ Proof.
   - apply Succ_Succb.
 Qed.
 
-Hint Rewrite H'_eq1  H'_eq2 : H'_rw.
+#[export] Hint Rewrite H'_eq1  H'_eq2 : H'_rw.
 
 Ltac lim_rw alpha := (assert (E0limit  alpha) by auto with E0);
                      rewrite (H'_eq3 alpha); auto with E0.

diff --git a/theories/ordinals/Epsilon0/L_alpha.v b/theories/ordinals/Epsilon0/L_alpha.v
@@ -14,7 +14,7 @@ From Equations Require Import Equations.
 Import RelationClasses Relations.
 
 #[global] Instance Olt : WellFounded E0lt := E0lt_wf.
-#[global] Hint Resolve Olt : E0.
+#[export] Hint Resolve Olt : E0.
 
 (** Using Coq-Equations for building a function which satisfies 
     [Large_sets.L_spec] *)
@@ -68,7 +68,7 @@ Proof.
 Qed.
 
 
-Hint Rewrite L_zero_eqn L_succ_eqn : L_rw.
+#[export] Hint Rewrite L_zero_eqn L_succ_eqn : L_rw.
 
 (* begin snippet Paraphrasesc:: no-out *)
 Lemma L_lim_eqn alpha i :