From 5d3d60e88f137183b4155bfa446dc7f3ebb35993 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 18:54:10 +0200
Subject: Fixing a bug of recursive notations introduced in dfdaf4de.

When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e5dbfcb4be..65efe228af 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -122,3 +122,5 @@ return (1, 2, 3, 4)
      : nat * nat * nat * nat
 {{ 1 | 1 // 1 }}
      : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b1015137d6..ea372ad1a3 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+
+(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
+Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
+Check !!! (x y:nat), True.
-- 
cgit v1.2.3