1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
From Coq Require Import Extraction.
Set Warnings "-extraction-inside-module".
Module OriginalExample.
Variant nondetE : Type -> Type :=
Or : nondetE bool.
Module Type MinSIG.
Parameter otherE : Type -> Type.
End MinSIG.
Module Min : MinSIG.
Definition otherE := nondetE.
End Min.
Extraction TestCompile Min.
End OriginalExample.
(**)
Module ExampleWithSmallParameter.
Variant nondetE : nat -> Type -> Type :=
Or : nondetE 0 bool.
Module Type MinSIG.
Parameter otherE : nat -> Type -> Type.
End MinSIG.
Module Min : MinSIG.
Definition otherE := nondetE.
End Min.
Extraction TestCompile Min.
End ExampleWithSmallParameter.
(* This was already working *)
Module ExampleWithLogicalDefinition.
Definition nondetE (n:nat) (X:Type) := Prop.
Module Type MinSIG.
Parameter otherE : nat -> Type -> Type.
End MinSIG.
Module Min : MinSIG.
Definition otherE := nondetE.
End Min.
Extraction TestCompile Min.
End ExampleWithLogicalDefinition.
|
