test-suite/bugs/closed/bug_1302.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

Module Type T.

Parameter A : Type.

Inductive L : Type :=
| L0 : L (* without this constructor, it works right *)
| L1 :  A -> L.

End T.

Axiom Tp : Type.

Module TT : T.

Definition A : Type := Tp.

Inductive L : Type :=
| L0 : L
| L1 :  A -> L.

End TT.