blob: da30a509acf81157f34beddc1faa7c5a4cd501fe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Module Type S.
Parameter t : Type.
Module M'.
Parameter t : Type.
Definition u := S.t.
End M'.
End S.
Module M : S.
Definition t := unit.
Module M'.
Definition t := bool.
Definition u := M.t.
End M'.
End M.
Require Extraction.
Fail Extraction TestCompile M.
|
