From 5c83e9be8a66f67628c022f2dec283a5b159b648 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Mar 2000 18:11:57 +0000
Subject: Retour sur les anciens noms

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@348 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Zarith/fast_integer.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v
index 444d5e9a15..93b78f9e44 100644
--- a/theories/Zarith/fast_integer.v
+++ b/theories/Zarith/fast_integer.v
@@ -258,7 +258,7 @@ Theorem compare_convert1 :
   ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL.
 Proof.
 Induction x;Induction y;Split;Simpl;Auto with arith;
-  (Discriminate Orelse (Elim (H y0); Auto with arith)).
+  (Discriminate Orelse (Elim (H p0); Auto with arith)).
 Save.
 
 Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y.
-- 
cgit v1.2.3