From f45a88ad054b88792ec8cc6631e4d4015fa95bab Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/vconv.mli')

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