Merge pull request #126 from ppedrot/rm-hint-constr

Remove the few instances of non-global hint declarations.

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.

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.