From 175a5b5ea593dba1897032d56a34ddc746973070 Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Mon, 11 Sep 2023 13:45:05 +0200
Subject: [PATCH] Add locality to Hint commands

---
 theories/ordinals/Epsilon0/Canon.v   | 4 ++--
 theories/ordinals/Epsilon0/Hprime.v  | 2 +-
 theories/ordinals/Epsilon0/L_alpha.v | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
index 8d693047..032656e3 100644
--- 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
index 5e59648f..6c495d2a 100644
--- 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
index c2e99703..e5b9af89 100644
--- 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 :