aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 248f68796..1a90139b4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -227,7 +227,8 @@ let parse_args is_ide =
| "-unsafe" :: [] -> usage ()
| "-debug" :: rem -> set_debug (); parse rem
-
+ | "-unboxed-values" :: rem -> Vm.set_transp_values true; parse rem
+ | "-no-vm" :: rem -> Reduction.use_vm := false;parse rem
| "-emacs" :: rem -> Options.print_emacs := true; parse rem
| "-where" :: _ -> print_endline Coq_config.coqlib; exit 0