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.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'kernel/vconv.mli') 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 -- cgit v1.2.3 From 44817bf722eacb0379bebc7e435bfafa503d574f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Oct 2015 14:21:45 +0200 Subject: Fix #4346 2/2: VM casts were not inferring universe constraints. --- kernel/vconv.mli | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'kernel/vconv.mli') diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 1a29a4d518..49e5d23e63 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,7 +12,11 @@ open Reduction (********************************************************************** s conversion functions *) -val vconv : conv_pb -> types conversion_function +val vm_conv : conv_pb -> types conversion_function -val val_of_constr : env -> constr -> values +(** A conversion function parametrized by a universe comparator. Used outside of + the kernel. *) +val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function +(** Precompute a VM value from a constr *) +val val_of_constr : env -> constr -> values -- cgit v1.2.3 From 672f8ee0c96584735294641bb4b8760e25197b80 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 14 Dec 2015 12:52:49 +0100 Subject: CLEANUP: in the Reduction module --- kernel/vconv.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vconv.mli') diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 49e5d23e63..acf4c408f3 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,7 +12,7 @@ open Reduction (********************************************************************** s conversion functions *) -val vm_conv : conv_pb -> types conversion_function +val vm_conv : conv_pb -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/vconv.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vconv.mli') diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 49e5d23e63..7e5397c069 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*