From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy 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`. --- lib/Integers.v | 47 +++++++++++++++++++++++++---------------------- 1 file changed, 25 insertions(+), 22 deletions(-) (limited to 'lib/Integers.v') 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 -- cgit