diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 08:37:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 08:37:18 +0000 |
| commit | 4c1a7a2238eef3f9ffa8a1253b506c86e2c442eb (patch) | |
| tree | ea3274550f221342e76bf482f5b02c7b43ac032d /test-suite/success/induct.v | |
| parent | 42331c8a1f29b97b6fa3300a667eea57deac86d0 (diff) | |
Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12359 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/induct.v')
| -rw-r--r-- | test-suite/success/induct.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index aae55ec7a..8e1a8d183 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -39,4 +39,5 @@ Lemma foo : forall n m : nat, n + m = n + m. Proof. intros; induction m as [|m] in n |- *. auto. + auto. Qed. |