From 48d15d0ac4851de879578eb2d62cf3de7b175230 Mon Sep 17 00:00:00 2001
From: jforest
Date: Fri, 23 Jun 2006 16:50:26 +0000
Subject: modifs de test-suite suite au passage des graphes de Function dans
 Type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8986 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Funind.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 939d06c773..133764c043 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -206,7 +206,7 @@ Qed.
 Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
 intros n m.
  functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
-rewrite <- hyp in H1; simpl in H1;tauto. 
+rewrite <- hyp in y; simpl in y;tauto. 
 inversion hyp.
 Qed.
  
@@ -280,14 +280,14 @@ destruct n. tauto.
 destruct n. inversion istr.
 destruct n. inversion istr.
 destruct n. tauto.
-simpl in *. inversion H1.
+simpl in *. inversion H0.
 Qed.
  
 Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
 intros n.
  functional induction isononeorfour n; intros m istr; inversion istr.
 apply istrue0.
-rewrite H in H0; simpl in H0;tauto.
+rewrite H in y; simpl in y;tauto.
 Qed.
  
 Function ftest4 (n m : nat) : nat :=
-- 
cgit v1.2.3