aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ArgumentsScope.v
blob: 13b5e13dd252d47b5669272a720dc3ce66a4bd94 (plain)
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
(* A few tests to check Argument Scope Global command *)

Section A.
Variable a : bool -> bool.
Definition negb' := negb.
Section B.
Variable b : bool -> bool.
Definition negb'' := negb.
About a.
About b.
About negb''.
About negb'.
About negb.
Arguments Scope Global negb'' [ _ ].
Arguments Scope Global negb' [ _ ].
Arguments Scope Global negb [ _ ].
Arguments Scope Global a [ _ ].
Arguments Scope Global b [ _ ].
About a.
About b.
About negb.
About negb'.
About negb''.
End B.
About a.
End A.
About negb.
About negb'.
About negb''.