aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-11-17 10:22:31 +0100
committerPierre-Marie Pédrot2014-11-17 10:22:31 +0100
commit659ca3902a144259ec449473e95df1b3eda1b6de (patch)
tree453864b590566eeb264792699ee24b87154dc684 /printing
parent364decf59c14ec8a672d3c4d46fa1939ea0e52d3 (diff)
Setting error tag on generic errors returned by Coqtop.
Diffstat (limited to 'printing')
-rw-r--r--printing/ppstyle.mli11
1 files changed, 11 insertions, 0 deletions
diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli
index 5fd9e074d8..700ec4314e 100644
--- a/printing/ppstyle.mli
+++ b/printing/ppstyle.mli
@@ -51,3 +51,14 @@ val init_color_output : unit -> unit
{!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
with additional syle information provided by this module. Be careful this is
not compatible with the Emacs mode! *)
+
+(** {5 Tags} *)
+
+val error_tag : t
+(** Tag used by the {!Pp.msg_error} function. *)
+
+val warning_tag : t
+(** Tag used by the {!Pp.msg_warning} function. *)
+
+val debug_tag : t
+(** Tag used by the {!Pp.msg_debug} function. *)