Remove -vm flag of coqtop.

Used to replace the standard conversion by the VM. Not so useful, and
implemented using a bunch of references inside and outside the kernel.

4 files changed, 0 insertions, 31 deletions

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 2cbc10202..27e184ea3 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -227,14 +227,3 @@ let vconv pb env t1 t2 =
   in ()
 
 let _ = Reduction.set_vm_conv vconv
-
-let use_vm = ref false
-
-let set_use_vm b =
-  use_vm := b;
-  if b then Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> vconv cv_pb)
-  else Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> Reduction.conv_cmp cv_pb)
-
-let use_vm _ = !use_vm
-
-
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 096d31ac8..1a29a4d51 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,8 +12,6 @@ open Reduction
 
 (**********************************************************************
   s conversion functions *)
-val use_vm : unit -> bool
-val set_use_vm : bool -> unit
 val vconv : conv_pb -> types conversion_function
 
 val val_of_constr : env -> constr -> values
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8925bbe29..72966a4ad 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -233,13 +233,6 @@ let compile_files () =
           compile_file vf)
         (List.rev l)
 
-(*s options for the virtual machine *)
-
-let use_vm = ref false
-
-let set_vm_opt () =
-  Vconv.set_use_vm !use_vm
-
 (** Options for proof general *)
 
 let set_emacs () =
@@ -547,7 +540,6 @@ let parse_args arglist =
     |"-unicode" -> add_require "Utf8_core"
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"-verbose-compat-notations" -> verb_compat_ntn := true
-    |"-vm" -> use_vm := true
     |"-where" -> print_where := true
 
     (* Deprecated options *)
@@ -607,7 +599,6 @@ let init arglist =
       if_verbose print_header ();
       inputstate ();
       Mltop.init_known_plugins ();
-      set_vm_opt ();
       engage ();
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 48100aa7f..f1f87ca9b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1347,15 +1347,6 @@ let _ =
       optwrite = Flags.make_universe_polymorphism }
 
 let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "use of virtual machine inside the kernel";
-      optkey   = ["Virtual";"Machine"];
-      optread  = (fun () -> Vconv.use_vm ());
-      optwrite = (fun b -> Vconv.set_use_vm b) }
-
-let _ =
   declare_int_option
     { optsync  = true;
       optdepr  = false;