diff options
Diffstat (limited to 'src/interactive.mli')
| -rw-r--r-- | src/interactive.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/interactive.mli b/src/interactive.mli index a092ee33..b1df0630 100644 --- a/src/interactive.mli +++ b/src/interactive.mli @@ -59,8 +59,6 @@ val ast : tannot defs ref val env : Env.t ref -val ir : Jib.cdef list ref - val arg : string -> string val command : string -> string |