diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/locate.out | 4 | ||||
| -rw-r--r-- | test-suite/output/locate.v | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 1ceec7c9f8..143eb1a1ae 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -9,3 +9,7 @@ Notation "( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) Notation "( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) +Notation +"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) +Notation +"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v index 262340e736..6995743531 100644 --- a/test-suite/output/locate.v +++ b/test-suite/output/locate.v @@ -19,4 +19,8 @@ Locate "( t , u , .. , v )". (* Was working though *) Locate "( _ , _ , .. , _ )". +(* We also support this *) +Locate "( t , u )". +Locate "( t , u , v )". + End N. |