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`.

10 files changed, 60 insertions, 60 deletions

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