Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
new file mode 100644
index 00000000..13b5e13d
--- /dev/null
+++ b/test-suite/output/ArgumentsScope.v
@@ -0,0 +1,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''.