diff options
| author | coqbot-app[bot] | 2020-11-16 14:19:09 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 14:19:09 +0000 |
| commit | fb186f25abeb0565bb6e238345f0c5147b697322 (patch) | |
| tree | 93bd3f7b69fd550112c34af2619251f72adef62e /test-suite | |
| parent | 1369d1426b0187bb817606966c32fdaf9afe4ed1 (diff) | |
| parent | 35ea1057b10c6457c1f9d5f61e8f72e35206392c (diff) | |
Merge PR #12690: Mini-fix of Locate for recursive notations using named variables.
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: SkySkimmer
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/locate.out | 6 | ||||
| -rw-r--r-- | test-suite/output/locate.v | 23 |
2 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 93d9d6cf7b..0196ead5e4 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,2 +1,8 @@ Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) Notation "x && y" := (andb x y) : bool_scope +Notation "'U' t" := (S t) (default interpretation) +Notation "'_' t" := (S t) (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) +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 af8b0ee193..6995743531 100644 --- a/test-suite/output/locate.v +++ b/test-suite/output/locate.v @@ -1,3 +1,26 @@ Set Printing Width 400. Notation "b1 && b2" := (if b1 then b2 else false). Locate "&&". + +Module M. + +Notation "'U' t" := (S t) (at level 0). +Notation "'_' t" := (S t) (at level 0). +Locate "U". (* was wrongly returning also "'_' t" *) +Locate "_". + +End M. + +Module N. + +(* Was not working at some time *) +Locate "( t , u , .. , v )". + +(* Was working though *) +Locate "( _ , _ , .. , _ )". + +(* We also support this *) +Locate "( t , u )". +Locate "( t , u , v )". + +End N. |