diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-28 18:32:57 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-28 18:32:57 +0000 |
| commit | 1ca3746894032d4372d7937b6b4188f8c4996c35 (patch) | |
| tree | cbe11477fd7bc6d89c52b97e79c4776d1255c2b1 /test-suite/success/Funind.v | |
| parent | 8e9e5320e58bfff85a1144122604bb1bc338ad9e (diff) | |
fixing a typo in the new Funinv.v test in test-suite/success
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Funind.v')
| -rw-r--r-- | test-suite/success/Funind.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 9e509a21d..740b8d669 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -1,5 +1,6 @@ Require Export Arith. - + + Fixpoint trivfun [n : nat] : nat := Cases n of O => O | (S m) => (trivfun m) end. @@ -8,7 +9,7 @@ Fixpoint trivfun [n : nat] : nat := Parameter varessai:nat. -Lemma first_try (trivfun varessai) = O. +Lemma first_try: (trivfun varessai) = O. Functional Induction trivfun varessai. Trivial. Simpl. |