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 <gaetan.gilbert@skyskimmer.net>

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.