diff options
Diffstat (limited to 'lib/interface.mli')
| -rw-r--r-- | lib/interface.mli | 8 |
1 files changed, 8 insertions, 0 deletions
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; } |