diff options
| author | Maxime Dénès | 2017-03-21 23:38:25 +0100 |
|---|---|---|
| committer | GitHub | 2017-03-21 23:38:25 +0100 |
| commit | 41e85ca95479ce1c8b4bf3832f6d6cb07e361655 (patch) | |
| tree | 0e334d7be38177c4ac33111a30b83b9ea3df3150 /mathcomp | |
| parent | 6a10f893dd9b662c25fefe1ab1e8344639dc6722 (diff) | |
| parent | c7c6619bfec5d8729e40a0b0848ded4251fd7e09 (diff) | |
Merge pull request #108 from ejgallego/pp_new_fix
Use pp_with as msg_with is being removed upstream.
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index a2371ad..3611b89 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -197,7 +197,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); + pp_with Format.str_formatter (prc c); let s = Format.flush_str_formatter () ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) |