aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/session.mli')
-rw-r--r--ide/session.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/session.mli b/ide/session.mli
index e99f08024..bb3816900 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -31,7 +31,7 @@ type session = {
buffer : GText.buffer;
script : Wg_ScriptView.script_view;
proof : Wg_ProofView.proof_view;
- messages : Wg_MessageView.message_view;
+ messages : Wg_RoutedMessageViews.message_views_router;
segment : Wg_Segment.segment;
fileops : FileOps.ops;
coqops : CoqOps.ops;