blob: bc5cd0fb683978f34ba2f0541db40a4b293565c3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Module Type E. Parameter T : Type. End E.
Module F (X:E).
#[universes(template)] 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) *)
|
