diff options
| author | Maxime Dénès | 2016-10-28 12:42:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-28 12:42:10 +0200 |
| commit | 3e98d3e4941f5098d743dffa8a032fd623a6a030 (patch) | |
| tree | ddfebc530ee37fce10f0cd6782c4504d9c20d486 /plugins | |
| parent | 40dbf1e0d8824fba357632addcdce434edc8b247 (diff) | |
| parent | cb5f55380875bb3029b051eb3acfbb912d83454b (diff) | |
Merge remote-tracking branch 'github/pr/319' into v8.6
Was PR#319: More error tagging, try to fix bug 5135
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 41eb5826b0..cf9a429455 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -112,8 +112,7 @@ let guard_term ch1 s i = match s.[i] with (* The call 'guard s i' should return true if the contents of s *) (* starting at i need bracketing to avoid ambiguities. *) let pr_guarded guard prc c = - msg_with Format.str_formatter (prc c); - let s = Format.flush_str_formatter () ^ "$" in + let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) let pr_constr = pr_constr |