blob: 4b3e7ff0543f536401cc8de276d926383dd63648 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Require Coq.extraction.Extraction.
Module Foo.
(* Definition foo := (I,I). *)
Definition bar := true.
End Foo.
Recursive Extraction Foo.bar.
Extraction TestCompile Foo.bar.
Module Foo'.
Definition foo := (I,I).
Definition bar := true.
End Foo'.
Recursive Extraction Foo'.bar.
Extraction TestCompile Foo'.bar.
Extraction Foo'.bar.
|
