diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-13 14:21:22 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-18 21:56:56 +0200 |
commit | cb5f55380875bb3029b051eb3acfbb912d83454b (patch) | |
tree | d13dfe3e824ee28e95c0325daa2db5002a5bd655 /plugins/ssrmatching | |
parent | 5ac6c86ad8e18161151d53687da1e2825f0a6b46 (diff) |
[pp] Use more convenient pp API in ssrmatching
Diffstat (limited to 'plugins/ssrmatching')
-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 4d1ac7139..21606b2d6 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 ~pp_tag:Ppstyle.pp_tag 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 |