aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4254.v
blob: ef219973df71904dde56e9dac67851b0a6f285d8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Inductive foo (V:Type):Type :=
  | Foo : list (bar V) -> foo V
with bar (V:Type): Type :=
  | bar1: bar V
  | bar2 : V -> bar V.

Module WithPoly.
Polymorphic Inductive foo (V:Type):Type :=
  | Foo : list (bar V) -> foo V
with bar (V:Type): Type :=
  | bar1: bar V
  | bar2 : V -> bar V.
End WithPoly.