aboutsummaryrefslogtreecommitdiff
path: root/ide/xmlprotocol.mli
diff options
context:
space:
mode:
authorEnrico Tassi2014-09-24 17:25:27 +0200
committerEnrico Tassi2014-09-29 21:54:31 +0200
commitec49447d078da25959d617ae23e55a668fdd1646 (patch)
treefa36169808ba6bcd886f9fa6e333a569e218717c /ide/xmlprotocol.mli
parent7eeda1b1ffd93311965aa431ea64f0fb38e3b34d (diff)
CoqIDE: new message to print AST
Diffstat (limited to 'ide/xmlprotocol.mli')
-rw-r--r--ide/xmlprotocol.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 42defce85b..145c88abbf 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -31,6 +31,7 @@ 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 abstract_eval_call : handler -> 'a call -> 'a value