Backtrack sur la révision #10401 : suppression de le_minus de la base de hints arith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10621 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 2 deletions

diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 8a62eb88b..a3b102055 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -124,12 +124,11 @@ Corollary le_minus : forall n m, n - m <= n.
 Proof.
   intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
 Qed.
-Hint Resolve le_minus: arith v62.
 
 Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
 Proof.
   intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
-    auto with arith.
+    auto using le_minus with arith.
     intros; absurd (0 < 0); auto with arith.
 Qed.
 Hint Resolve lt_minus: arith v62.