aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ArgumentsScope.v
blob: 1ff53294e515ed3c1cc624a02acb7fc4f3dc778a (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 Global Argument Scope 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.
Global Arguments Scope negb'' [ _ ].
Global Arguments Scope negb' [ _ ].
Global Arguments Scope negb [ _ ].
Global Arguments Scope a [ _ ].
Global Arguments Scope b [ _ ].
About a.
About b.
About negb.
About negb'.
About negb''.
End B.
About a.
End A.
About negb.
About negb'.
About negb''.