diff options
Diffstat (limited to 'lib/serialize.mli')
| -rw-r--r-- | lib/serialize.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/serialize.mli b/lib/serialize.mli index 2b1718bf76..e749462087 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -29,6 +29,8 @@ val get_options : get_options_sty -> get_options_rty call val set_options : set_options_sty -> set_options_rty call val quit : quit_sty -> quit_rty call val init : init_sty -> init_rty call +(* retrocompatibility *) +val interp : interp_sty -> interp_rty call val abstract_eval_call : handler -> 'a call -> 'a value |