From 3eb1ae56f9f2ee380e6cc323ab2cbaeb45cdf386 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Dec 2001 01:57:08 +0000
Subject: Amélioration nommage hypothèses NewInduction (et incompatibilités)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Between.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories')

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index e6b4446017..1c08cdba37 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -126,8 +126,8 @@ Qed.
 
 Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l).
 Proof.
-NewInduction 1; Intros.
-Elim H1; Auto with arith.
+NewDestruct 1; Intros.
+Elim H0; Auto with arith.
 Qed.
 
 Lemma between_or_exists : 
-- 
cgit v1.2.3