From 043d67c93111328fdbc2d7afa1a84daf3d68a5cc Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Oct 2015 13:41:00 +0200
Subject: Remove unused infos structure in VM.

Became unused after c47b205206d832430fa80a3386be80149e281d33.
---
 kernel/vconv.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 8af2efc588..2cbc102021 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -40,8 +40,6 @@ let conv_vect fconv vect1 vect2 cu =
     !rcu
   else raise NotConvertible
 
-let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
-
 let rec conv_val env pb k v1 v2 cu =
   if v1 == v2 then cu
   else conv_whd env pb k (whd_val v1) (whd_val v2) cu
@@ -219,7 +217,6 @@ and conv_eq_vect env vt1 vt2 cu =
   else raise NotConvertible
 
 let vconv pb env t1 t2 =
-  infos := create_clos_infos betaiotazeta env;
   let _cu =
     try conv_eq env pb t1 t2 (universes env)
     with NotConvertible ->
-- 
cgit v1.2.3


From f45a88ad054b88792ec8cc6631e4d4015fa95bab Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Oct 2015 13:45:06 +0200
Subject: 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.
---
 kernel/vconv.ml | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'kernel/vconv.ml')

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
-
-
-- 
cgit v1.2.3