diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/ArgumentsScope.v | 12 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v index 13b5e13dd2..1ff53294e5 100644 --- a/test-suite/output/ArgumentsScope.v +++ b/test-suite/output/ArgumentsScope.v @@ -1,4 +1,4 @@ -(* A few tests to check Argument Scope Global command *) +(* A few tests to check Global Argument Scope command *) Section A. Variable a : bool -> bool. @@ -11,11 +11,11 @@ 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 [ _ ]. +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. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 63f85bc707..4bdd579a60 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -30,4 +30,4 @@ Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2). (* Check import of notations from within a section *) Notation "+1 x" := (S x) (at level 25, x at level 9). -Section A. Notation Global "'Z'" := O (at level 9). End A. +Section A. Global Notation "'Z'" := O (at level 9). End A. |