diff options
Diffstat (limited to 'test-suite/output/ArgumentsScope.v')
| -rw-r--r-- | test-suite/output/ArgumentsScope.v | 29 |
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''. |