From eb5b610ec2b2d2707951b20daa9f701ebf346215 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 7 Apr 2024 14:12:02 +0200 Subject: [PATCH] Remove the few instances of non-global hint declarations. These commands are fragile and trigger a warning. --- theory/cut_minus.v | 9 ++++++--- theory/ring_ideals.v | 6 +++++- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/theory/cut_minus.v b/theory/cut_minus.v index ec5dd63..32e5233 100644 --- a/theory/cut_minus.v +++ b/theory/cut_minus.v @@ -12,7 +12,8 @@ Section cut_minus_properties. Local Existing Instance pseudo_srorder_semiring. Add Ring SR: (rings.stdlib_semiring_theory R). - Hint Resolve (@orders.le_flip R _ _). + Let local_le_flip := @orders.le_flip R _ _. + Hint Resolve local_le_flip. Global Instance cut_minus_proper: Proper ((=) ==> (=) ==> (=)) cut_minus | 1. Proof. @@ -30,8 +31,10 @@ Section cut_minus_properties. Global Instance cut_minus_mor_2: ∀ x : R, Setoid_Morphism (∸ x) | 0. Proof. split; try apply _. solve_proper. Qed. - Hint Resolve (cut_minus_0). - Hint Resolve (cut_minus_le). + Let local_cut_minus_0 := (cut_minus_0). + Let local_cut_minus_le := (cut_minus_le). + Hint Resolve local_cut_minus_0. + Hint Resolve local_cut_minus_le. Lemma cut_minus_diag x : x ∸ x = 0. Proof. now apply cut_minus_0. Qed. diff --git a/theory/ring_ideals.v b/theory/ring_ideals.v index cd5ecff..b0853e7 100644 --- a/theory/ring_ideals.v +++ b/theory/ring_ideals.v @@ -20,8 +20,12 @@ Section ideal_congruence. Context `{ideal : RingIdeal A P}. Add Ring A2 : (rings.stdlib_ring_theory A). + Let local_ideal_closed_plus_negate := (ideal_closed_plus_negate). + Let local_ideal_closed_mult_l := (ideal_closed_mult_l). + Let local_ideal_closed_mult_r := (ideal_closed_mult_r). + (* If P is an ideal, we can easily derive some further closedness properties: *) - Hint Resolve (ideal_closed_plus_negate) (ideal_closed_mult_l) (ideal_closed_mult_r). + Hint Resolve local_ideal_closed_plus_negate local_ideal_closed_mult_l local_ideal_closed_mult_r. Lemma ideal_closed_0 : P 0. Proof. destruct ideal_NonEmpty as [[x Px]]. rewrite <-(plus_negate_r x). intuition. Qed.