From 7a9205cd226c1df6a52afaee3374bc9cdffd6e8c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Aug 2017 22:28:28 +0200
Subject: Adding a test for #5569 (warning about skipping spaces).

The two previous commits make the warning irrelevant and useless.
---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index c66f801223..e5dbfcb4be 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -120,3 +120,5 @@ where
 letpair x [1] = {0};
 return (1, 2, 3, 4)
      : nat * nat * nat * nat
+{{ 1 | 1 // 1 }}
+     : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 58f9e15abc..b1015137d6 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -180,3 +180,9 @@ Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )"
 Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
   (let x:=a in ( .. (b0,b1) .., b2)).
 Check letpair x [1] = {0}; return (1,2,3,4).
+
+(* Test spacing in #5569 *)
+
+Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
+  (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
+Check 1+1+1.
-- 
cgit v1.2.3