aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/metasyntax.ml')
-rw-r--r--vernac/metasyntax.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 567fc57fa..f5b31e89d 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1056,7 +1056,7 @@ module SynData = struct
extra : (string * string) list;
(* XXX: Callback to printing, must remove *)
- msgs : ((std_ppcmds -> unit) * std_ppcmds) list;
+ msgs : ((Pp.t -> unit) * Pp.t) list;
(* Fields for internalization *)
recvars : (Id.t * Id.t) list;