diff options
| author | Pierre-Marie Pédrot | 2016-01-24 12:35:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-24 12:37:38 +0100 |
| commit | cb30837323aa462df24ad6668790f67b9bf20b5d (patch) | |
| tree | 58f171b3ac23b52abecb5617fad57cab29d6f41f | |
| parent | 4b1103dc38754917e12bf04feca446e02cf55f07 (diff) | |
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.
| -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 *) |