diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/locate.out | 13 | ||||
| -rw-r--r-- | test-suite/output/locate.v | 19 |
2 files changed, 30 insertions, 2 deletions
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 93d9d6cf7b..1ceec7c9f8 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,2 +1,11 @@ -Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) -Notation "x && y" := (andb x y) : bool_scope +Notation +"b1 && b2" := if b1 then b2 else false (default interpretation) +"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) diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v index af8b0ee193..262340e736 100644 --- a/test-suite/output/locate.v +++ b/test-suite/output/locate.v @@ -1,3 +1,22 @@ 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 "( _ , _ , .. , _ )". + +End N. |