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