diff options
Diffstat (limited to 'src/interactive.mli')
| -rw-r--r-- | src/interactive.mli | 2 |
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 |
