summaryrefslogtreecommitdiff
path: root/src/interactive.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/interactive.mli')
-rw-r--r--src/interactive.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/interactive.mli b/src/interactive.mli
index 46b52022..0b087dc7 100644
--- a/src/interactive.mli
+++ b/src/interactive.mli
@@ -57,7 +57,7 @@ val opt_emacs_mode : bool ref
val opt_suppress_banner : bool ref
val opt_auto_interpreter_rewrites : bool ref
-val ast : tannot defs ref
+val ast : tannot ast ref
val env : Env.t ref