From 60d15dc5f56411c53f6974c4df900b4ce59da23f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 14 Jul 2020 16:02:07 +0200 Subject: Fixing Locate for recursive notations with names. E.g. Locate "(x , y , .. , z )" now works while only Locate "(_ , _ , .. , _ )" was working before. This also fixes a confusion between a variable and its anonymization into _, wrongly finding notations mentioning '_'. Co-authored-by: Gaëtan Gilbert --- test-suite/output/locate.out | 13 +++++++++++-- test-suite/output/locate.v | 19 +++++++++++++++++++ 2 files changed, 30 insertions(+), 2 deletions(-) (limited to 'test-suite') 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. -- cgit v1.2.3 From 5b7a1d7d6a7b3281bfb28c8548edb85bc99c91ab Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 14 Jul 2020 16:54:20 +0200 Subject: Adding support for Locate "( x , y )". It finds "( x , y , .. , z )". Co-authored-by: Gaëtan Gilbert --- test-suite/output/locate.out | 4 ++++ test-suite/output/locate.v | 4 ++++ 2 files changed, 8 insertions(+) (limited to 'test-suite') 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. -- cgit v1.2.3 From 35ea1057b10c6457c1f9d5f61e8f72e35206392c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 19 Jul 2020 13:00:03 +0200 Subject: Ensuring the body of the notation in Locate is printed at level 0. This is consistent with the syntax of Notation and is (IMO) clearer. --- test-suite/output/locate.out | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) (limited to 'test-suite') diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 143eb1a1ae..0196ead5e4 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,15 +1,8 @@ -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) -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 "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) -- cgit v1.2.3