From 98f6a9d847f4fac14696f51096c8334c9bffda6f Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 20 Sep 2009 14:02:58 +0000 Subject: 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 --- test-suite/success/induct.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'test-suite/success') 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. -- cgit v1.2.3