1 files changed, 27 insertions, 1 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 2aec6e9b..8e1a8d18 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -5,7 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* Teste des definitions inductives imbriquees *)
+
+(* Test des definitions inductives imbriquees *)
 
 Require Import List.
 
@@ -15,3 +16,28 @@ Inductive X : Set :=
 Inductive Y : Set :=
     cons2 : list (Y * Y) -> Y.
 
+(* Test inductive types with local definitions *)
+
+Inductive eq1 : forall A:Type, let B:=A in A -> Prop :=
+  refl1 : eq1 True I.
+
+Check
+ fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
+   let B := A in
+     fun (a : A) (e : eq1 A a) =>
+       match e in (eq1 A0 B0 a0) return (P A0 a0) with
+       | refl1 => f
+       end.
+
+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.
+  auto.
+Qed.