aboutsummaryrefslogtreecommitdiff
path: root/lib/interface.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/interface.mli')
-rw-r--r--lib/interface.mli12
1 files changed, 6 insertions, 6 deletions
diff --git a/lib/interface.mli b/lib/interface.mli
index f655921d78..349f7baf98 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -103,14 +103,14 @@ type coq_info = {
compile_date : string;
}
-(** * Coq answers to CoqIde *)
+(** Coq messages *)
type message_level =
-| Debug of string
-| Info
-| Notice
-| Warning
-| Error
+ | Debug of string
+ | Info
+ | Notice
+ | Warning
+ | Error
type message = {
message_level : message_level;