blob: 4b6916af552e2c4355a4bdd16e6d263f33e752a3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Module Type E. Parameter T : Type. End E.
Module F (X:E).
Inductive foo := box : X.T -> foo.
End F.
Module ME. Definition T := nat. End ME.
Module A := F ME.
(* Note: A.foo could live in Set, and coqchk sees that (because of
template polymorphism implementation details) *)
|
