From cb30837323aa462df24ad6668790f67b9bf20b5d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 24 Jan 2016 12:35:49 +0100
Subject: Fixing bug #4495: Failed assertion in metasyntax.ml.

We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
---
 test-suite/bugs/closed/4495.v | 1 +
 toplevel/metasyntax.ml        | 7 ++++++-
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4495.v

diff --git a/test-suite/bugs/closed/4495.v b/test-suite/bugs/closed/4495.v
new file mode 100644
index 0000000000..8b032db5f5
--- /dev/null
+++ b/test-suite/bugs/closed/4495.v
@@ -0,0 +1 @@
+Fail Notation "'forall' x  ..  y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ae82b64e87..231b22e255 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -540,10 +540,15 @@ let add_break_if_none n = function
   | l -> UnpCut (PpBrk(n,0)) :: l
 
 let check_open_binder isopen sl m =
+  let pr_token = function
+  | Terminal s -> str s
+  | Break n -> str "␣"
+  | _ -> assert false
+  in
   if isopen && not (List.is_empty sl) then
     errorlabstrm "" (str "as " ++ pr_id m ++
       str " is a non-closed binder, no such \"" ++
-      prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
+      prlist_with_sep spc pr_token sl
       ++ strbrk "\" is allowed to occur.")
 
 (* Heuristics for building default printing rules *)
-- 
cgit v1.2.3