test-suite/failure/subtyping.v


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.

Fail End TT.