From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 21 Jan 2021 15:44:09 +0100
Subject: Qualify `Hint` as `Global Hint` where appropriate

This avoids a new warning of Coq 8.13.

Eventually these `Global Hint` should become `#[export] Hint`,
with a cleaner but different meaning than `Global Hint`.
---
 MenhirLib/Validator_classes.v  |  8 +++----
 MenhirLib/Validator_complete.v |  6 +++---
 aarch64/Asmgenproof1.v         |  4 ++--
 aarch64/Conventions1.v         |  2 +-
 arm/Asmgenproof1.v             |  6 +++---
 arm/Conventions1.v             |  2 +-
 backend/Asmgenproof0.v         | 12 +++++------
 backend/CSEdomain.v            |  4 ++--
 backend/CminorSel.v            |  4 ++--
 backend/Cminortyping.v         | 12 +++++------
 backend/Deadcodeproof.v        |  2 +-
 backend/NeedDomain.v           | 10 ++++-----
 backend/RTLgenproof.v          |  4 ++--
 backend/RTLgenspec.v           | 48 +++++++++++++++++++++---------------------
 backend/ValueAnalysis.v        |  4 ++--
 backend/ValueDomain.v          | 20 +++++++++---------
 cfrontend/Ctyping.v            |  8 +++----
 common/Events.v                |  2 +-
 common/Memory.v                |  2 +-
 common/Memtype.v               |  2 +-
 common/Separation.v            |  2 +-
 common/Unityping.v             |  6 +++---
 common/Values.v                | 10 ++++-----
 lib/Coqlib.v                   | 20 +++++++++---------
 lib/Integers.v                 | 47 ++++++++++++++++++++++-------------------
 lib/Intv.v                     |  2 +-
 powerpc/Asmgenproof1.v         | 14 ++++++------
 powerpc/Conventions1.v         |  2 +-
 riscV/Asmgenproof1.v           |  2 +-
 x86/Conventions1.v             |  2 +-
 30 files changed, 136 insertions(+), 133 deletions(-)

diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v
index d8063123..781a6aa6 100644
--- a/MenhirLib/Validator_classes.v
+++ b/MenhirLib/Validator_classes.v
@@ -17,7 +17,7 @@ Require Import Alphabet.
 
 Class IsValidator (P : Prop) (b : bool) :=
   is_validator : b = true -> P.
-Hint Mode IsValidator + - : typeclass_instances.
+Global Hint Mode IsValidator + - : typeclass_instances.
 
 Instance is_validator_true : IsValidator True true.
 Proof. done. Qed.
@@ -55,12 +55,12 @@ Qed.
 
 (* We do not use an instance directly here, because we need somehow to
    force Coq to instantiate b with a lambda. *)
-Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
+Global Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
     eapply (is_validator_forall_finite _ _ (fun (x:A) => _))
   : typeclass_instances.
 
 (* Hint for synthetizing pattern-matching. *)
-Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
+Global Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
     let b := fresh "b" in
     unshelve notypeclasses refine (let b : bool := _ in _);
       [destruct u; intros; shelve|];    (* Synthetize `match .. with` in the validator. *)
@@ -71,5 +71,5 @@ Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
 (* Hint for unfolding definitions. This is necessary because many
   hints for IsValidator use [Hint Extern], which do not automatically
   unfold identifiers. *)
-Hint Extern 100 (IsValidator ?X _) => unfold X
+Global Hint Extern 100 (IsValidator ?X _) => unfold X
   : typeclass_instances.
diff --git a/MenhirLib/Validator_complete.v b/MenhirLib/Validator_complete.v
index 9ba3e53c..ac4dd0c4 100644
--- a/MenhirLib/Validator_complete.v
+++ b/MenhirLib/Validator_complete.v
@@ -140,7 +140,7 @@ Qed.
 (* We do not declare this lemma as an instance, and use [Hint Extern]
    instead, because the typeclass mechanism has trouble instantiating
    some evars if we do not explicitely call [eassumption]. *)
-Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
+Global Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
   eapply is_validator_state_has_future_subset; [eassumption|eassumption || reflexivity|]
 : typeclass_instances.
 
@@ -171,7 +171,7 @@ Proof.
   - destruct (b lookahead). by destruct b'. exfalso. by induction l; destruct b'.
   - eauto.
 Qed.
-Hint Extern 100 (IsValidator _ _) =>
+Global Hint Extern 100 (IsValidator _ _) =>
   match goal with
   | H : TerminalSet.In ?lookahead ?lset |- _ =>
     eapply (is_validator_iterate_lset _ (fun lookahead => _) _ _ H); clear H
@@ -238,7 +238,7 @@ Proof.
     revert EQ. unfold future_of_prod=>-> //.
 Qed.
 (* We need a hint for expplicitely instantiating b1 and b2 with lambdas. *)
-Hint Extern 0 (IsValidator
+Global Hint Extern 0 (IsValidator
                  (forall st prod fut lookahead,
                      state_has_future st prod fut lookahead -> _)
                  _) =>
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 5f27f6bf..93c1f1ed 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -26,7 +26,7 @@ Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC.
 Proof.
   destruct r; simpl; congruence.
 Qed.
-Hint Resolve preg_of_iregsp_not_PC: asmgen.
+Global Hint Resolve preg_of_iregsp_not_PC: asmgen.
 
 Lemma preg_of_not_X16: forall r, preg_of r <> X16.
 Proof.
@@ -44,7 +44,7 @@ Proof.
   intros. apply ireg_of_not_X16 in H. congruence.
 Qed.
 
-Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen.
+Global Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen.
 
 (** Useful simplification tactic *)
 
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v
index 7edb16dd..f401458c 100644
--- a/aarch64/Conventions1.v
+++ b/aarch64/Conventions1.v
@@ -335,7 +335,7 @@ Proof.
   eapply loc_arguments_rec_charact; eauto. lia.
 Qed.
 
-Hint Resolve loc_arguments_acceptable: locs.
+Global Hint Resolve loc_arguments_acceptable: locs.
 
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index fce9d4a6..b94964a0 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -40,14 +40,14 @@ Lemma ireg_of_not_R14:
 Proof.
   intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
-Hint Resolve ireg_of_not_R14: asmgen.
+Global Hint Resolve ireg_of_not_R14: asmgen.
 
 Lemma ireg_of_not_R14':
   forall m r, ireg_of m = OK r -> r <> IR14.
 Proof.
   intros. generalize (ireg_of_not_R14 _ _ H). congruence.
 Qed.
-Hint Resolve ireg_of_not_R14': asmgen.
+Global Hint Resolve ireg_of_not_R14': asmgen.
 
 (** [undef_flags] and [nextinstr_nf] *)
 
@@ -75,7 +75,7 @@ Proof.
   intros; red; intros; subst; discriminate.
 Qed.
 
-Hint Resolve data_if_preg if_preg_not_PC: asmgen.
+Global Hint Resolve data_if_preg if_preg_not_PC: asmgen.
 
 Lemma nextinstr_nf_inv:
   forall r rs, if_preg r = true -> (nextinstr_nf rs)#r = rs#r.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index b94ce9ef..0ddd882f 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -427,7 +427,7 @@ Proof.
   destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
 Qed.
 
-Hint Resolve loc_arguments_acceptable: locs.
+Global Hint Resolve loc_arguments_acceptable: locs.
 
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 5e8acd6f..85cee14f 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -31,7 +31,7 @@ Require Import Conventions.
 
 (** * Processor registers and register states *)
 
-Hint Extern 2 (_ <> _) => congruence: asmgen.
+Global Hint Extern 2 (_ <> _) => congruence: asmgen.
 
 Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
@@ -56,7 +56,7 @@ Lemma preg_of_data:
 Proof.
   intros. destruct r; reflexivity.
 Qed.
-Hint Resolve preg_of_data: asmgen.
+Global Hint Resolve preg_of_data: asmgen.
 
 Lemma data_diff:
   forall r r',
@@ -64,7 +64,7 @@ Lemma data_diff:
 Proof.
   congruence.
 Qed.
-Hint Resolve data_diff: asmgen.
+Global Hint Resolve data_diff: asmgen.
 
 Lemma preg_of_not_SP:
   forall r, preg_of r <> SP.
@@ -78,7 +78,7 @@ Proof.
   intros. apply data_diff; auto with asmgen.
 Qed.
 
-Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
+Global Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
 
 Lemma nextinstr_pc:
   forall rs, (nextinstr rs)#PC = Val.offset_ptr rs#PC Ptrofs.one.
@@ -746,7 +746,7 @@ Qed.
 Definition nolabel (i: instruction) :=
   match i with Plabel _ => False | _ => True end.
 
-Hint Extern 1 (nolabel _) => exact I : labels.
+Global Hint Extern 1 (nolabel _) => exact I : labels.
 
 Lemma tail_nolabel_cons:
   forall i c k,
@@ -757,7 +757,7 @@ Proof.
   intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
 Qed.
 
-Hint Resolve tail_nolabel_refl: labels.
+Global Hint Resolve tail_nolabel_refl: labels.
 
 Ltac TailNoLabel :=
   eauto with labels;
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index 9b1243c8..e96c4cd4 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -92,7 +92,7 @@ Record wf_numbering (n: numbering) : Prop := {
       In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v
 }.
 
-Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.
+Global Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.
 
 (** Satisfiability of numberings.  A numbering holds in a concrete
   execution state if there exists a valuation assigning values to
@@ -130,7 +130,7 @@ Record numbering_holds (valu: valuation) (ge: genv) (sp: val)
      n.(num_reg)!r = Some v -> rs#r = valu v
 }.
 
-Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse.
+Global Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse.
 
 Lemma empty_numbering_holds:
   forall valu ge sp rs m,
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 5cbdc249..f6f6e34d 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -464,7 +464,7 @@ Inductive final_state: state -> int -> Prop :=
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
-Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
+Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
 
 (** * Lifting of let-bound variables *)
 
@@ -580,4 +580,4 @@ Proof.
   eexact H. apply insert_lenv_0.
 Qed.
 
-Hint Resolve eval_lift: evalexpr.
+Global Hint Resolve eval_lift: evalexpr.
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index 92ec45f2..9f35fe35 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -290,7 +290,7 @@ Lemma expect_incr: forall te e t1 t2 e',
 Proof.
   unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto.
 Qed.
-Hint Resolve expect_incr: ty.
+Global Hint Resolve expect_incr: ty.
 
 Lemma expect_sound: forall e t1 t2 e',
   expect e t1 t2 = OK e' -> t1 = t2.
@@ -305,7 +305,7 @@ Proof.
 - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
 - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
 Qed.
-Hint Resolve type_expr_incr: ty.
+Global Hint Resolve type_expr_incr: ty.
 
 Lemma type_expr_sound: forall te a t e e',
     type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t.
@@ -325,7 +325,7 @@ Lemma type_exprlist_incr: forall te al tl e e',
 Proof.
   induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T; eauto with ty.
 Qed.
-Hint Resolve type_exprlist_incr: ty.
+Global Hint Resolve type_exprlist_incr: ty.
 
 Lemma type_exprlist_sound: forall te al tl e e',
     type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl.
@@ -342,7 +342,7 @@ Proof.
 - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
 - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
 Qed.
-Hint Resolve type_assign_incr: ty.
+Global Hint Resolve type_assign_incr: ty.
 
 Lemma type_assign_sound: forall te id a e e',
     type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id).
@@ -362,7 +362,7 @@ Lemma opt_set_incr: forall te optid optty e e',
 Proof.
   unfold opt_set; intros. destruct optid, optty; try (monadInv H); eauto with ty.
 Qed.
-Hint Resolve opt_set_incr: ty.
+Global Hint Resolve opt_set_incr: ty.
 
 Lemma opt_set_sound: forall te optid sg e e',
     opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' ->
@@ -379,7 +379,7 @@ Proof.
   induction s; simpl; intros e1 e2 T SAT; try (monadInv T); eauto with ty.
 - destruct tret, o; try (monadInv T); eauto with ty.
 Qed.
-Hint Resolve type_stmt_incr: ty.
+Global Hint Resolve type_stmt_incr: ty.
 
 Lemma type_stmt_sound: forall te tret s e e',
     type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s.
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 7aa6ff88..7be12c69 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -358,7 +358,7 @@ Proof.
   intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto.
 Qed.
 
-Hint Resolve add_need_all_eagree add_need_all_lessdef
+Global Hint Resolve add_need_all_eagree add_need_all_lessdef
              add_need_eagree add_need_vagree
              add_needs_all_eagree add_needs_all_lessdef
              add_needs_eagree add_needs_vagree
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index d3c6ed75..fc1ae16d 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -74,7 +74,7 @@ Proof.
   intros. simpl in H. auto.
 Qed.
 
-Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
+Global Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
 
 Inductive vagree_list: list val -> list val -> list nval -> Prop :=
   | vagree_list_nil: forall nvl,
@@ -100,7 +100,7 @@ Proof.
   destruct nvl; constructor; auto with na.
 Qed.
 
-Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
+Global Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
 
 (** ** Ordering and least upper bound between value needs *)
 
@@ -116,8 +116,8 @@ Proof.
   destruct x; constructor; auto.
 Qed.
 
-Hint Constructors nge: na.
-Hint Resolve nge_refl: na.
+Global Hint Constructors nge: na.
+Global Hint Resolve nge_refl: na.
 
 Lemma nge_trans: forall x y, nge x y -> forall z, nge y z -> nge x z.
 Proof.
@@ -1084,7 +1084,7 @@ Proof.
   intros. apply H.
 Qed.
 
-Hint Resolve nreg_agree: na.
+Global Hint Resolve nreg_agree: na.
 
 Lemma eagree_ge:
   forall e1 e2 ne ne',
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 88f7fe53..1602823f 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -165,7 +165,7 @@ Proof.
   subst r0; contradiction.
   apply Regmap.gso; auto.
 Qed.
-Hint Resolve match_env_update_temp: rtlg.
+Global Hint Resolve match_env_update_temp: rtlg.
 
 (** Matching between environments is preserved by simultaneous
   assignment to a Cminor local variable (in the Cminor environments)
@@ -205,7 +205,7 @@ Proof.
   eapply match_env_update_temp; eauto.
   eapply match_env_update_var; eauto.
 Qed.
-Hint Resolve match_env_update_dest: rtlg.
+Global Hint Resolve match_env_update_dest: rtlg.
 
 (** A variant of [match_env_update_var] corresponding to the assignment
   of the result of a builtin. *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 72693f63..25f9954c 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -128,7 +128,7 @@ Ltac monadInv H :=
 
 (** * Monotonicity properties of the state *)
 
-Hint Resolve state_incr_refl: rtlg.
+Global Hint Resolve state_incr_refl: rtlg.
 
 Lemma instr_at_incr:
   forall s1 s2 n i,
@@ -137,7 +137,7 @@ Proof.
   intros. inv H.
   destruct (H3 n); congruence.
 Qed.
-Hint Resolve instr_at_incr: rtlg.
+Global Hint Resolve instr_at_incr: rtlg.
 
 (** The following tactic saturates the hypotheses with
   [state_incr] properties that follow by transitivity from
@@ -174,14 +174,14 @@ Lemma valid_fresh_absurd:
 Proof.
   intros r s. unfold reg_valid, reg_fresh; case r; tauto.
 Qed.
-Hint Resolve valid_fresh_absurd: rtlg.
+Global Hint Resolve valid_fresh_absurd: rtlg.
 
 Lemma valid_fresh_different:
   forall r1 r2 s, reg_valid r1 s -> reg_fresh r2 s -> r1 <> r2.
 Proof.
   unfold not; intros. subst r2. eauto with rtlg.
 Qed.
-Hint Resolve valid_fresh_different: rtlg.
+Global Hint Resolve valid_fresh_different: rtlg.
 
 Lemma reg_valid_incr:
   forall r s1 s2, state_incr s1 s2 -> reg_valid r s1 -> reg_valid r s2.
@@ -190,7 +190,7 @@ Proof.
   inversion INCR.
   unfold reg_valid. intros; apply Plt_Ple_trans with (st_nextreg s1); auto.
 Qed.
-Hint Resolve reg_valid_incr: rtlg.
+Global Hint Resolve reg_valid_incr: rtlg.
 
 Lemma reg_fresh_decr:
   forall r s1 s2, state_incr s1 s2 -> reg_fresh r s2 -> reg_fresh r s1.
@@ -199,7 +199,7 @@ Proof.
   unfold reg_fresh; unfold not; intros.
   apply H4. apply Plt_Ple_trans with (st_nextreg s1); auto.
 Qed.
-Hint Resolve reg_fresh_decr: rtlg.
+Global Hint Resolve reg_fresh_decr: rtlg.
 
 (** Validity of a list of registers. *)
 
@@ -211,7 +211,7 @@ Lemma regs_valid_nil:
 Proof.
   intros; red; intros. elim H.
 Qed.
-Hint Resolve regs_valid_nil: rtlg.
+Global Hint Resolve regs_valid_nil: rtlg.
 
 Lemma regs_valid_cons:
   forall r1 rl s,
@@ -232,7 +232,7 @@ Lemma regs_valid_incr:
 Proof.
   unfold regs_valid; intros; eauto with rtlg.
 Qed.
-Hint Resolve regs_valid_incr: rtlg.
+Global Hint Resolve regs_valid_incr: rtlg.
 
 (** A register is ``in'' a mapping if it is associated with a Cminor
   local or let-bound variable. *)
@@ -253,7 +253,7 @@ Lemma map_valid_incr:
 Proof.
   unfold map_valid; intros; eauto with rtlg.
 Qed.
-Hint Resolve map_valid_incr: rtlg.
+Global Hint Resolve map_valid_incr: rtlg.
 
 (** * Properties of basic operations over the state *)
 
@@ -265,7 +265,7 @@ Lemma add_instr_at:
 Proof.
   intros. monadInv H. simpl. apply PTree.gss.
 Qed.
-Hint Resolve add_instr_at: rtlg.
+Global Hint Resolve add_instr_at: rtlg.
 
 (** Properties of [update_instr]. *)
 
@@ -278,7 +278,7 @@ Proof.
   destruct (check_empty_node s1 n); try discriminate.
   inv H. simpl. apply PTree.gss.
 Qed.
-Hint Resolve update_instr_at: rtlg.
+Global Hint Resolve update_instr_at: rtlg.
 
 (** Properties of [new_reg]. *)
 
@@ -289,7 +289,7 @@ Proof.
   intros. monadInv H.
   unfold reg_valid; simpl. apply Plt_succ.
 Qed.
-Hint Resolve new_reg_valid: rtlg.
+Global Hint Resolve new_reg_valid: rtlg.
 
 Lemma new_reg_fresh:
   forall s1 s2 r i,
@@ -299,7 +299,7 @@ Proof.
   unfold reg_fresh; simpl.
   exact (Plt_strict _).
 Qed.
-Hint Resolve new_reg_fresh: rtlg.
+Global Hint Resolve new_reg_fresh: rtlg.
 
 Lemma new_reg_not_in_map:
   forall s1 s2 m r i,
@@ -307,7 +307,7 @@ Lemma new_reg_not_in_map:
 Proof.
   unfold not; intros; eauto with rtlg.
 Qed.
-Hint Resolve new_reg_not_in_map: rtlg.
+Global Hint Resolve new_reg_not_in_map: rtlg.
 
 (** * Properties of operations over compilation environments *)
 
@@ -330,7 +330,7 @@ Proof.
   intros. inv H0. left; exists name; auto.
   intros. inv H0.
 Qed.
-Hint Resolve find_var_in_map: rtlg.
+Global Hint Resolve find_var_in_map: rtlg.
 
 Lemma find_var_valid:
   forall s1 s2 map name r i,
@@ -338,7 +338,7 @@ Lemma find_var_valid:
 Proof.
   eauto with rtlg.
 Qed.
-Hint Resolve find_var_valid: rtlg.
+Global Hint Resolve find_var_valid: rtlg.
 
 (** Properties of [find_letvar]. *)
 
@@ -350,7 +350,7 @@ Proof.
   caseEq (nth_error (map_letvars map) idx); intros; monadInv H0.
   right; apply nth_error_in with idx; auto.
 Qed.
-Hint Resolve find_letvar_in_map: rtlg.
+Global Hint Resolve find_letvar_in_map: rtlg.
 
 Lemma find_letvar_valid:
   forall s1 s2 map idx r i,
@@ -358,7 +358,7 @@ Lemma find_letvar_valid:
 Proof.
   eauto with rtlg.
 Qed.
-Hint Resolve find_letvar_valid: rtlg.
+Global Hint Resolve find_letvar_valid: rtlg.
 
 (** Properties of [add_var]. *)
 
@@ -445,7 +445,7 @@ Proof.
   intros until r.  unfold alloc_reg.
   case a; eauto with rtlg.
 Qed.
-Hint Resolve alloc_reg_valid: rtlg.
+Global Hint Resolve alloc_reg_valid: rtlg.
 
 Lemma alloc_reg_fresh_or_in_map:
   forall map a s r s' i,
@@ -469,7 +469,7 @@ Proof.
   apply regs_valid_nil.
   apply regs_valid_cons. eauto with rtlg. eauto with rtlg.
 Qed.
-Hint Resolve alloc_regs_valid: rtlg.
+Global Hint Resolve alloc_regs_valid: rtlg.
 
 Lemma alloc_regs_fresh_or_in_map:
   forall map al s rl s' i,
@@ -494,7 +494,7 @@ Proof.
   intros until r.  unfold alloc_reg.
   case dest; eauto with rtlg.
 Qed.
-Hint Resolve alloc_optreg_valid: rtlg.
+Global Hint Resolve alloc_optreg_valid: rtlg.
 
 Lemma alloc_optreg_fresh_or_in_map:
   forall map dest s r s' i,
@@ -609,7 +609,7 @@ Proof.
   apply regs_valid_cons; eauto with rtlg.
 Qed.
 
-Hint Resolve new_reg_target_ok alloc_reg_target_ok
+Global Hint Resolve new_reg_target_ok alloc_reg_target_ok
              alloc_regs_target_ok: rtlg.
 
 (** The following predicate is a variant of [target_reg_ok] used
@@ -631,7 +631,7 @@ Lemma return_reg_ok_incr:
 Proof.
   induction 1; intros; econstructor; eauto with rtlg.
 Qed.
-Hint Resolve return_reg_ok_incr: rtlg.
+Global Hint Resolve return_reg_ok_incr: rtlg.
 
 Lemma new_reg_return_ok:
   forall s1 r s2 map sig i,
@@ -676,7 +676,7 @@ Inductive reg_map_ok: mapping -> reg -> option ident -> Prop :=
       map.(map_vars)!id = Some rd ->
       reg_map_ok map rd (Some id).
 
-Hint Resolve reg_map_ok_novar: rtlg.
+Global Hint Resolve reg_map_ok_novar: rtlg.
 
 (** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c],
   between nodes [ns] and [nd], contains instructions that compute the
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index f7e4f0ed..ebf2c5ea 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -342,7 +342,7 @@ Proof.
   induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto.
 Qed.
 
-Hint Resolve areg_sound aregs_sound: va.
+Global Hint Resolve areg_sound aregs_sound: va.
 
 Lemma abuiltin_arg_sound:
   forall bc ge rs sp m ae rm am,
@@ -1912,7 +1912,7 @@ Proof.
 - exact NOSTACK.
 Qed.
 
-Hint Resolve areg_sound aregs_sound: va.
+Global Hint Resolve areg_sound aregs_sound: va.
 
 (** * Interface with other optimizations *)
 
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 45894bfc..01f080ff 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -43,12 +43,12 @@ Proof.
   elim H. apply H0; auto.
 Qed.
 
-Hint Extern 2 (_ = _) => congruence : va.
-Hint Extern 2 (_ <> _) => congruence : va.
-Hint Extern 2 (_ < _) => extlia : va.
-Hint Extern 2 (_ <= _) => extlia : va.
-Hint Extern 2 (_ > _) => extlia : va.
-Hint Extern 2 (_ >= _) => extlia : va.
+Global Hint Extern 2 (_ = _) => congruence : va.
+Global Hint Extern 2 (_ <> _) => congruence : va.
+Global Hint Extern 2 (_ < _) => extlia : va.
+Global Hint Extern 2 (_ <= _) => extlia : va.
+Global Hint Extern 2 (_ > _) => extlia : va.
+Global Hint Extern 2 (_ >= _) => extlia : va.
 
 Section MATCH.
 
@@ -4711,10 +4711,10 @@ Module VA <: SEMILATTICE.
 
 End VA.
 
-Hint Constructors cmatch : va.
-Hint Constructors pmatch: va.
-Hint Constructors vmatch: va.
-Hint Resolve cnot_sound symbol_address_sound
+Global Hint Constructors cmatch : va.
+Global Hint Constructors pmatch: va.
+Global Hint Constructors vmatch: va.
+Global Hint Resolve cnot_sound symbol_address_sound
        shl_sound shru_sound shr_sound
        and_sound or_sound xor_sound notint_sound
        ror_sound rolm_sound
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 83f3cfe0..87e3506c 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -537,9 +537,9 @@ Inductive wt_program : program -> Prop :=
          wt_fundef p.(prog_comp_env) e fd) ->
       wt_program p.
 
-Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
-Hint Extern 1 (wt_int _ _ _) => exact I: ty.
-Hint Extern 1 (wt_int _ _ _) => reflexivity: ty.
+Global Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
+Global Hint Extern 1 (wt_int _ _ _) => exact I: ty.
+Global Hint Extern 1 (wt_int _ _ _) => reflexivity: ty.
 
 Ltac DestructCases :=
   match goal with
@@ -955,7 +955,7 @@ Proof.
   destruct (classify_bool t); congruence.
 Qed.
 
-Hint Resolve check_cast_sound check_bool_sound: ty.
+Global Hint Resolve check_cast_sound check_bool_sound: ty.
 
 Lemma check_arguments_sound:
   forall el tl x, check_arguments el tl = OK x -> wt_arguments el tl.
diff --git a/common/Events.v b/common/Events.v
index ee2d529d..aae0662c 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1697,7 +1697,7 @@ Qed.
 
 End EVAL_BUILTIN_ARG.
 
-Hint Constructors eval_builtin_arg: barg.
+Global Hint Constructors eval_builtin_arg: barg.
 
 (** Invariance by change of global environment. *)
 
diff --git a/common/Memory.v b/common/Memory.v
index 641a9243..b16a98b6 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -4500,7 +4500,7 @@ Notation mem := Mem.mem.
 
 Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes.
 
-Hint Resolve
+Global Hint Resolve
   Mem.valid_not_valid_diff
   Mem.perm_implies
   Mem.perm_cur
diff --git a/common/Memtype.v b/common/Memtype.v
index ca9c6f1f..1d6f252b 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -60,7 +60,7 @@ Inductive perm_order: permission -> permission -> Prop :=
   | perm_W_R:   perm_order Writable Readable
   | perm_any_N: forall p, perm_order p Nonempty.
 
-Hint Constructors perm_order: mem.
+Global Hint Constructors perm_order: mem.
 
 Lemma perm_order_trans:
   forall p1 p2 p3, perm_order p1 p2 -> perm_order p2 p3 -> perm_order p1 p3.
diff --git a/common/Separation.v b/common/Separation.v
index 0357b2bf..bf134a18 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -113,7 +113,7 @@ Proof.
   intros P Q [[A B] [C D]]. split; auto.
 Qed.
 
-Hint Resolve massert_imp_refl massert_eqv_refl : core.
+Global Hint Resolve massert_imp_refl massert_eqv_refl : core.
 
 (** * Separating conjunction *)
 
diff --git a/common/Unityping.v b/common/Unityping.v
index 878e5943..6dbd3c48 100644
--- a/common/Unityping.v
+++ b/common/Unityping.v
@@ -199,7 +199,7 @@ Proof.
   apply A. rewrite PTree.gso by congruence. auto.
 Qed.
 
-Hint Resolve set_incr: ty.
+Global Hint Resolve set_incr: ty.
 
 Lemma set_sound:
   forall te x ty e e', set e x ty = OK e' -> satisf te e' -> te x = ty.
@@ -216,7 +216,7 @@ Proof.
   induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty.
 Qed.
 
-Hint Resolve set_list_incr: ty.
+Global Hint Resolve set_list_incr: ty.
 
 Lemma set_list_sound:
   forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> map te xl = tyl.
@@ -242,7 +242,7 @@ Proof.
 - inv H; simpl in *; split; auto.
 Qed.
 
-Hint Resolve move_incr: ty.
+Global Hint Resolve move_incr: ty.
 
 Lemma move_sound:
   forall te e r1 r2 e' changed,
diff --git a/common/Values.v b/common/Values.v
index c5b07e2f..f8a666c0 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -2000,7 +2000,7 @@ Inductive lessdef_list: list val -> list val -> Prop :=
       lessdef v1 v2 -> lessdef_list vl1 vl2 ->
       lessdef_list (v1 :: vl1) (v2 :: vl2).
 
-Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core.
+Global Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core.
 
 Lemma lessdef_list_inv:
   forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1.
@@ -2225,7 +2225,7 @@ Inductive inject (mi: meminj): val -> val -> Prop :=
   | val_inject_undef: forall v,
       inject mi Vundef v.
 
-Hint Constructors inject : core.
+Global Hint Constructors inject : core.
 
 Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
   | inject_list_nil :
@@ -2234,7 +2234,7 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
       inject mi v v' -> inject_list mi vl vl'->
       inject_list mi (v :: vl) (v' :: vl').
 
-Hint Resolve inject_list_nil inject_list_cons : core.
+Global Hint Resolve inject_list_nil inject_list_cons : core.
 
 Lemma inject_ptrofs:
   forall mi i, inject mi (Vptrofs i) (Vptrofs i).
@@ -2242,7 +2242,7 @@ Proof.
   unfold Vptrofs; intros. destruct Archi.ptr64; auto.
 Qed.
 
-Hint Resolve inject_ptrofs : core.
+Global Hint Resolve inject_ptrofs : core.
 
 Section VAL_INJ_OPS.
 
@@ -2545,7 +2545,7 @@ Proof.
   constructor. eapply val_inject_incr; eauto. auto.
 Qed.
 
-Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core.
+Global Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core.
 
 Lemma val_inject_lessdef:
   forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2.
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index ae9dceec..bd52d20a 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -116,7 +116,7 @@ Lemma Plt_ne:
 Proof.
   unfold Plt; intros. red; intro. subst y. eelim Pos.lt_irrefl; eauto.
 Qed.
-Hint Resolve Plt_ne: coqlib.
+Global Hint Resolve Plt_ne: coqlib.
 
 Lemma Plt_trans:
   forall (x y z: positive), Plt x y -> Plt y z -> Plt x z.
@@ -127,14 +127,14 @@ Lemma Plt_succ:
 Proof.
   unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl.
 Qed.
-Hint Resolve Plt_succ: coqlib.
+Global Hint Resolve Plt_succ: coqlib.
 
 Lemma Plt_trans_succ:
   forall (x y: positive), Plt x y -> Plt x (Pos.succ y).
 Proof.
   intros. apply Plt_trans with y. assumption. apply Plt_succ.
 Qed.
-Hint Resolve Plt_succ: coqlib.
+Global Hint Resolve Plt_succ: coqlib.
 
 Lemma Plt_succ_inv:
   forall (x y: positive), Plt x (Pos.succ y) -> Plt x y \/ x = y.
@@ -175,7 +175,7 @@ Proof (Pos.lt_le_trans).
 Lemma Plt_strict: forall p, ~ Plt p p.
 Proof (Pos.lt_irrefl).
 
-Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib.
+Global Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib.
 
 Ltac extlia := unfold Plt, Ple in *; lia.
 
@@ -559,7 +559,7 @@ Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C :=
 
 (** Properties of [List.nth] (n-th element of a list). *)
 
-Hint Resolve in_eq in_cons: coqlib.
+Global Hint Resolve in_eq in_cons: coqlib.
 
 Lemma nth_error_in:
   forall (A: Type) (n: nat) (l: list A) (x: A),
@@ -573,14 +573,14 @@ Proof.
     discriminate.
     apply in_cons. auto.
 Qed.
-Hint Resolve nth_error_in: coqlib.
+Global Hint Resolve nth_error_in: coqlib.
 
 Lemma nth_error_nil:
   forall (A: Type) (idx: nat), nth_error (@nil A) idx = None.
 Proof.
   induction idx; simpl; intros; reflexivity.
 Qed.
-Hint Resolve nth_error_nil: coqlib.
+Global Hint Resolve nth_error_nil: coqlib.
 
 (** Compute the length of a list, with result in [Z]. *)
 
@@ -671,7 +671,7 @@ Lemma incl_cons_inv:
 Proof.
   unfold incl; intros. apply H. apply in_cons. auto.
 Qed.
-Hint Resolve incl_cons_inv: coqlib.
+Global Hint Resolve incl_cons_inv: coqlib.
 
 Lemma incl_app_inv_l:
   forall (A: Type) (l1 l2 m: list A),
@@ -687,7 +687,7 @@ Proof.
   unfold incl; intros. apply H. apply in_or_app. right; assumption.
 Qed.
 
-Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
+Global Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
 
 Lemma incl_same_head:
   forall (A: Type) (x: A) (l1 l2: list A),
@@ -1042,7 +1042,7 @@ Proof.
   constructor. constructor. constructor. auto.
 Qed.
 
-Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
+Global Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
 
 Lemma is_tail_incl:
   forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
diff --git a/lib/Integers.v b/lib/Integers.v
index 03f19c98..9368b531 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -91,7 +91,7 @@ Proof.
   generalize modulus_gt_one; lia.
 Qed.
 
-Hint Resolve modulus_pos: ints.
+Global Hint Resolve modulus_pos: ints.
 
 (** * Representation of machine integers *)
 
@@ -400,45 +400,45 @@ Definition eqm := eqmod modulus.
 
 Lemma eqm_refl: forall x, eqm x x.
 Proof (eqmod_refl modulus).
-Hint Resolve eqm_refl: ints.
+Global Hint Resolve eqm_refl: ints.
 
 Lemma eqm_refl2:
   forall x y, x = y -> eqm x y.
 Proof (eqmod_refl2 modulus).
-Hint Resolve eqm_refl2: ints.
+Global Hint Resolve eqm_refl2: ints.
 
 Lemma eqm_sym: forall x y, eqm x y -> eqm y x.
 Proof (eqmod_sym modulus).
-Hint Resolve eqm_sym: ints.
+Global Hint Resolve eqm_sym: ints.
 
 Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z.
 Proof (eqmod_trans modulus).
-Hint Resolve eqm_trans: ints.
+Global Hint Resolve eqm_trans: ints.
 
 Lemma eqm_small_eq:
   forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y.
 Proof (eqmod_small_eq modulus).
-Hint Resolve eqm_small_eq: ints.
+Global Hint Resolve eqm_small_eq: ints.
 
 Lemma eqm_add:
   forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d).
 Proof (eqmod_add modulus).
-Hint Resolve eqm_add: ints.
+Global Hint Resolve eqm_add: ints.
 
 Lemma eqm_neg:
   forall x y, eqm x y -> eqm (-x) (-y).
 Proof (eqmod_neg modulus).
-Hint Resolve eqm_neg: ints.
+Global Hint Resolve eqm_neg: ints.
 
 Lemma eqm_sub:
   forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d).
 Proof (eqmod_sub modulus).
-Hint Resolve eqm_sub: ints.
+Global Hint Resolve eqm_sub: ints.
 
 Lemma eqm_mult:
   forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d).
 Proof (eqmod_mult modulus).
-Hint Resolve eqm_mult: ints.
+Global Hint Resolve eqm_mult: ints.
 
 Lemma eqm_same_bits:
   forall x y,
@@ -466,7 +466,7 @@ Lemma eqm_unsigned_repr:
 Proof.
   unfold eqm; intros. rewrite unsigned_repr_eq. apply eqmod_mod. auto with ints.
 Qed.
-Hint Resolve eqm_unsigned_repr: ints.
+Global Hint Resolve eqm_unsigned_repr: ints.
 
 Lemma eqm_unsigned_repr_l:
   forall a b, eqm a b -> eqm (unsigned (repr a)) b.
@@ -474,7 +474,7 @@ Proof.
   intros. apply eqm_trans with a.
   apply eqm_sym. apply eqm_unsigned_repr. auto.
 Qed.
-Hint Resolve eqm_unsigned_repr_l: ints.
+Global Hint Resolve eqm_unsigned_repr_l: ints.
 
 Lemma eqm_unsigned_repr_r:
   forall a b, eqm a b -> eqm a (unsigned (repr b)).
@@ -482,7 +482,7 @@ Proof.
   intros. apply eqm_trans with b. auto.
   apply eqm_unsigned_repr.
 Qed.
-Hint Resolve eqm_unsigned_repr_r: ints.
+Global Hint Resolve eqm_unsigned_repr_r: ints.
 
 Lemma eqm_signed_unsigned:
   forall x, eqm (signed x) (unsigned x).
@@ -497,7 +497,7 @@ Theorem unsigned_range:
 Proof.
   destruct i. simpl. lia.
 Qed.
-Hint Resolve unsigned_range: ints.
+Global Hint Resolve unsigned_range: ints.
 
 Theorem unsigned_range_2:
   forall i, 0 <= unsigned i <= max_unsigned.
@@ -505,7 +505,7 @@ Proof.
   intro; unfold max_unsigned.
   generalize (unsigned_range i). lia.
 Qed.
-Hint Resolve unsigned_range_2: ints.
+Global Hint Resolve unsigned_range_2: ints.
 
 Theorem signed_range:
   forall i, min_signed <= signed i <= max_signed.
@@ -524,7 +524,7 @@ Proof.
   destruct i; simpl. unfold repr. apply mkint_eq.
   rewrite Z_mod_modulus_eq. apply Z.mod_small; lia.
 Qed.
-Hint Resolve repr_unsigned: ints.
+Global Hint Resolve repr_unsigned: ints.
 
 Lemma repr_signed:
   forall i, repr (signed i) = i.
@@ -532,7 +532,7 @@ Proof.
   intros. transitivity (repr (unsigned i)).
   apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints.
 Qed.
-Hint Resolve repr_signed: ints.
+Global Hint Resolve repr_signed: ints.
 
 Opaque repr.
 
@@ -547,7 +547,7 @@ Proof.
   intros. rewrite unsigned_repr_eq.
   apply Z.mod_small. unfold max_unsigned in H. lia.
 Qed.
-Hint Resolve unsigned_repr: ints.
+Global Hint Resolve unsigned_repr: ints.
 
 Theorem signed_repr:
   forall z, min_signed <= z <= max_signed -> signed (repr z) = z.
@@ -4802,7 +4802,7 @@ Qed.
 
 End AGREE64.
 
-Hint Resolve
+Global Hint Resolve
   agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq
   agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs
   agree64_repr agree64_of_int agree64_of_int_eq
@@ -4816,19 +4816,22 @@ Notation ptrofs := Ptrofs.int.
 
 Global Opaque Ptrofs.repr.
 
-Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans
+Global Hint Resolve
+  Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans
   Int.eqm_small_eq Int.eqm_add Int.eqm_neg Int.eqm_sub Int.eqm_mult
   Int.eqm_unsigned_repr Int.eqm_unsigned_repr_l Int.eqm_unsigned_repr_r
   Int.unsigned_range Int.unsigned_range_2
   Int.repr_unsigned Int.repr_signed Int.unsigned_repr : ints.
 
-Hint Resolve Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans
+Global Hint Resolve
+  Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans
   Int64.eqm_small_eq Int64.eqm_add Int64.eqm_neg Int64.eqm_sub Int64.eqm_mult
   Int64.eqm_unsigned_repr Int64.eqm_unsigned_repr_l Int64.eqm_unsigned_repr_r
   Int64.unsigned_range Int64.unsigned_range_2
   Int64.repr_unsigned Int64.repr_signed Int64.unsigned_repr : ints.
 
-Hint Resolve Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans
+Global Hint Resolve
+  Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans
   Ptrofs.eqm_small_eq Ptrofs.eqm_add Ptrofs.eqm_neg Ptrofs.eqm_sub Ptrofs.eqm_mult
   Ptrofs.eqm_unsigned_repr Ptrofs.eqm_unsigned_repr_l Ptrofs.eqm_unsigned_repr_r
   Ptrofs.unsigned_range Ptrofs.unsigned_range_2
diff --git a/lib/Intv.v b/lib/Intv.v
index 19943942..82d3c751 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -303,7 +303,7 @@ Qed.
 
 (** Hints *)
 
-Hint Resolve
+Global Hint Resolve
   notin_range range_notin
   is_notempty empty_notin in_notempty
   disjoint_sym empty_disjoint_r empty_disjoint_l
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 14ca22f9..89514d62 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -132,7 +132,7 @@ Lemma important_diff:
 Proof.
   congruence.
 Qed.
-Hint Resolve important_diff: asmgen.
+Global Hint Resolve important_diff: asmgen.
 
 Lemma important_data_preg_1:
   forall r, data_preg r = true -> important_preg r = true.    
@@ -146,7 +146,7 @@ Proof.
   intros. destruct (data_preg r) eqn:E; auto. apply important_data_preg_1 in E. congruence.
 Qed.  
 
-Hint Resolve important_data_preg_1 important_data_preg_2: asmgen.
+Global Hint Resolve important_data_preg_1 important_data_preg_2: asmgen.
 
 Lemma nextinstr_inv2:
   forall r rs, important_preg r = true -> (nextinstr rs)#r = rs#r.
@@ -166,7 +166,7 @@ Lemma gpr_or_zero_zero:
 Proof.
   intros. reflexivity.
 Qed.
-Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen.
+Global Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen.
 
 Lemma gpr_or_zero_l_not_zero:
   forall rs r, r <> GPR0 -> gpr_or_zero_l rs r = rs#r.
@@ -178,21 +178,21 @@ Lemma gpr_or_zero_l_zero:
 Proof.
   intros. reflexivity.
 Qed.
-Hint Resolve gpr_or_zero_l_not_zero gpr_or_zero_l_zero: asmgen.
+Global Hint Resolve gpr_or_zero_l_not_zero gpr_or_zero_l_zero: asmgen.
 
 Lemma ireg_of_not_GPR0:
   forall m r, ireg_of m = OK r -> IR r <> IR GPR0.
 Proof.
   intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
-Hint Resolve ireg_of_not_GPR0: asmgen.
+Global Hint Resolve ireg_of_not_GPR0: asmgen.
 
 Lemma ireg_of_not_GPR0':
   forall m r, ireg_of m = OK r -> r <> GPR0.
 Proof.
   intros. generalize (ireg_of_not_GPR0 _ _ H). congruence.
 Qed.
-Hint Resolve ireg_of_not_GPR0': asmgen.
+Global Hint Resolve ireg_of_not_GPR0': asmgen.
 
 (** Useful properties of the LR register *)
 
@@ -208,7 +208,7 @@ Proof.
   intros. rewrite preg_notin_charact. intros. apply preg_of_not_LR. 
 Qed.
 
-Hint Resolve preg_of_not_LR preg_notin_LR: asmgen.
+Global Hint Resolve preg_of_not_LR preg_notin_LR: asmgen.
       
 (** Useful simplification tactic *)
 
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 56beffe8..f05e77df 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -341,7 +341,7 @@ Proof.
   unfold forall_rpair; destruct p; intuition auto.
 Qed.
 
-Hint Resolve loc_arguments_acceptable: locs.
+Global Hint Resolve loc_arguments_acceptable: locs.
 
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 253e769f..8195ce44 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -88,7 +88,7 @@ Proof.
   intros. apply ireg_of_not_X31 in H. congruence.
 Qed.
 
-Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen.
+Global Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen.
 
 (** Useful simplification tactic *)
 
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index e3c51f60..a4e3b970 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -423,7 +423,7 @@ Proof.
   unfold forall_rpair; destruct p; intuition auto.
 Qed.
 
-Hint Resolve loc_arguments_acceptable: locs.
+Global Hint Resolve loc_arguments_acceptable: locs.
 
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
-- 
cgit