aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssreflect.ml42
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 *)