blob: 7c8af1e46e411758f9d02be0c0088803945afa5c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* Bug 5177 https://coq.inria.fr/bug/5177 :
Extraction and module type containing application and "with" *)
Module Type T.
Parameter t: Type.
End T.
Module Type A (MT: T).
Parameter t1: Type.
Parameter t2: Type.
Parameter bar: MT.t -> t1 -> t2.
End A.
Module MakeA(MT: T): A MT with Definition t1 := nat.
Definition t1 := nat.
Definition t2 := nat.
Definition bar (m: MT.t) (x:t1) := x.
End MakeA.
Require Extraction.
Recursive Extraction MakeA.
Extraction TestCompile MakeA.
|
