aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/subtyping.v
blob: 35fd20369fa83c6cab6fedb825a98dd7e64f4222 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(* A variant of bug #1302 that must fail *)

Module Type T.

 Parameter A : Type.

 Inductive L : Prop := 
 | L0
 | L1 :  (A -> Prop) -> L.

End T.

Module TT : T. 

 Parameter A : Type.

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

End TT.