diff options
| author | Hugo Herbelin | 2020-07-14 16:54:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-15 21:07:58 +0100 |
| commit | 5b7a1d7d6a7b3281bfb28c8548edb85bc99c91ab (patch) | |
| tree | eec163aa8a80346da497711ef10ab100d5686c78 /test-suite | |
| parent | 60d15dc5f56411c53f6974c4df900b4ce59da23f (diff) | |
Adding support for Locate "( x , y )".
It finds "( x , y , .. , z )".
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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. |