blob: 231d103a598d15e0cfbb107bd911aca0ea69685d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* 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.
|
