Fix #9569 (notations collect the spine binding variables at printing time).

This allows to know which global references whose basename may be
unexpectedly caught need to be qualified.

Note: the alternative strategy, which is sometimes used, of renaming
the binding variables so as to avoid collisions with the basename of a
global reference is somehow less nice.

2 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out
new file mode 100644
index 0000000000..2d474e4933
--- /dev/null
+++ b/test-suite/output/bug_9569.out
@@ -0,0 +1,16 @@
+1 subgoal
+  
+  ============================
+  exists I : True, I = Logic.I
+1 subgoal
+  
+  ============================
+  f True False True False (Logic.True /\ Logic.False)
+1 subgoal
+  
+  ============================
+  [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I]
+1 subgoal
+  
+  ============================
+  [I & I = Logic.I | I = Logic.I; Logic.I = I]
diff --git a/test-suite/output/bug_9569.v b/test-suite/output/bug_9569.v
new file mode 100644
index 0000000000..ee5b052811
--- /dev/null
+++ b/test-suite/output/bug_9569.v
@@ -0,0 +1,18 @@
+Goal exists I, I = Logic.I.
+Show.
+Abort.
+
+Notation f x y p q r := ((forall x, p /\ r) /\ forall y, q /\ r).
+Goal f True False True False (Logic.True /\ Logic.False).
+Show.
+Abort.
+
+Notation "[ x | y ; z ; .. ; t ]" := (pair .. (pair (forall x, y) (forall x, z)) .. (forall x, t)).
+Goal [ I | I = Logic.I ; I = Logic.I ] = [ I | I = Logic.I ; I = Logic.I ].
+Show.
+Abort.
+
+Notation "[ x & p | y ; .. ; z ; t ]" := (forall x, p -> y -> .. (forall x, p -> z -> forall x, p -> t) ..).
+Goal [ I & I = Logic.I | I = Logic.I ; Logic.I = I ].
+Show.
+Abort.