From d5451ad4fc55c38ea0a7a1687dfc80c2bb0f9d13 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 25 Nov 2013 10:13:32 +0100
Subject: First stab at retrocompatible INTERP message

---
 lib/interface.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'lib/interface.mli')

diff --git a/lib/interface.mli b/lib/interface.mli
index 31577e6296..24f2b65249 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -233,6 +233,12 @@ type about_rty = coq_info
 type handle_exn_sty = exn
 type handle_exn_rty = state_id * location * string
 
+(* Retrocompatibility stuff *)
+type interp_sty = (raw * verbose) * string
+(* spiwack: [Inl] for safe and [Inr] for unsafe. *)
+type interp_rty = (string,string) Util.union
+
+
 type handler = {
   add         : add_sty         -> add_rty;
   edit_at     : edit_at_sty     -> edit_at_rty;
@@ -250,5 +256,7 @@ type handler = {
   handle_exn  : handle_exn_sty  -> handle_exn_rty;
   init        : init_sty        -> init_rty;
   quit        : quit_sty        -> quit_rty;
+  (* Retrocompatibility stuff *)
+  interp      : interp_sty      -> interp_rty;
 }
 
-- 
cgit v1.2.3