diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-20 14:02:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-20 14:02:58 +0000 |
| commit | 98f6a9d847f4fac14696f51096c8334c9bffda6f (patch) | |
| tree | 3ab3dabe0f93f38b17434976f0b0c9833b8e3ff5 /test-suite/success/induct.v | |
| parent | fbcd19a076f255614012fd076863ca296c1b2626 (diff) | |
Only one "in" clause in "destruct" even for a multiple "destruct".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12348 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/induct.v')
| -rw-r--r-- | test-suite/success/induct.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index b78651c91..aae55ec7a 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -32,3 +32,11 @@ Check Inductive eq2 (A:Type) (a:A) : forall B C:Type, let D:=(A*B*C)%type in D -> Prop := refl2 : eq2 A a unit bool (a,tt,true). + +(* Check that induction variables are cleared even with in clause *) + +Lemma foo : forall n m : nat, n + m = n + m. +Proof. + intros; induction m as [|m] in n |- *. + auto. +Qed. |