diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-23 16:50:26 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-23 16:50:26 +0000 |
| commit | 48d15d0ac4851de879578eb2d62cf3de7b175230 (patch) | |
| tree | d8ec95df9f0db4ae3282d6e3d2d096ce75b1c30f | |
| parent | 3dfe56ca4de86e1e4e7779a4ac0534f36909644e (diff) | |
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
| -rw-r--r-- | test-suite/success/Funind.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 939d06c77..133764c04 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 := |