blob: 1979eda820d3b51f79a8264acd68b7d14fd6379b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
Module Type Intf1.
Parameter T : Type.
Inductive a := A.
End Intf1.
Module Impl1 <: Intf1.
Definition T := unit.
Inductive a := A.
End Impl1.
Module Type Intf2
(Impl1 : Intf1).
Parameter x : Impl1.A=Impl1.A -> Impl1.T.
End Intf2.
Module Type Intf3
(Impl1 : Intf1)
(Impl2 : Intf2(Impl1)).
End Intf3.
Fail Module Toto
(Impl1' : Intf1)
(Impl2 : Intf2(Impl1'))
(Impl3 : Intf3(Impl1)(Impl2)).
(* A UserError is expected here, not an uncaught Not_found *)
(* NB : the Inductive above and the A=A weren't in the initial test,
they are here only to force an access to the environment
(cf [Printer.qualid_of_global]) and check that this env is ok. *)
|
