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`.
---
 powerpc/Asmgenproof1.v | 14 +++++++-------
 powerpc/Conventions1.v |  2 +-
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'powerpc')

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