diff options
| -rw-r--r-- | test-suite/bugs/closed/4495.v | 1 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 7 |
2 files changed, 7 insertions, 1 deletions
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 *) |