diff options
Diffstat (limited to 'ide/xmlprotocol.mli')
| -rw-r--r-- | ide/xmlprotocol.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 145c88abbf..b6677d8745 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -31,7 +31,8 @@ val init : init_sty -> init_rty call val stop_worker : stop_worker_sty -> stop_worker_rty call (* retrocompatibility *) val interp : interp_sty -> interp_rty call -val print_ast : print_ast_sty -> print_ast_rty call +val print_ast : print_ast_sty -> print_ast_rty call +val annotate : annotate_sty -> annotate_rty call val abstract_eval_call : handler -> 'a call -> 'a value |