aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3287.v
blob: 7c78131252d4f6ef90b12b004fcaf3ddb7d8414b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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.