2 files changed, 0 insertions, 13 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 2cbc102021..27e184ea3f 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 096d31ac81..1a29a4d518 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