From 49623ae29421c2ccd16f82d71b65cfacd0877fec Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 5 Mar 2008 19:22:22 +0000
Subject: 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
---
 theories/Arith/Minus.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 8a62eb88ba..a3b102055c 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.
-- 
cgit v1.2.3