diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 15:44:09 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 17:17:18 +0100 |
| commit | fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 (patch) | |
| tree | fdfd03a7f16fea070848ad9911373dbb4d603fc2 /powerpc | |
| parent | eca149363d20d94198a4b1e1ae4f9f964e468098 (diff) | |
| download | compcert-kvx-fc82b6c80fd3feeb4ef9478e6faa16b5b1104593.tar.gz compcert-kvx-fc82b6c80fd3feeb4ef9478e6faa16b5b1104593.zip | |
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`.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 14 | ||||
| -rw-r--r-- | powerpc/Conventions1.v | 2 |
2 files changed, 8 insertions, 8 deletions
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. |