From 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 8 Oct 2015 18:06:55 +0200 Subject: Fix #4346 1/2: native casts were not inferring universe constraints. --- kernel/nativeconv.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'kernel/nativeconv.mli') diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 318a7d830b..21f0b2e9e5 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -12,3 +12,7 @@ open Nativelambda (** This module implements the conversion test by compiling to OCaml code *) val native_conv : conv_pb -> evars -> types conversion_function + +(** A conversion function parametrized by a universe comparator. Used outside of + the kernel. *) +val native_conv_gen : conv_pb -> evars -> (constr, 'a) generic_conversion_function -- 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/nativeconv.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/nativeconv.mli') diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 21f0b2e9e5..4dddb9fd30 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -15,4 +15,4 @@ val native_conv : conv_pb -> evars -> types conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) -val native_conv_gen : conv_pb -> evars -> (constr, 'a) generic_conversion_function +val native_conv_gen : conv_pb -> evars -> (types, 'a) generic_conversion_function -- 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/nativeconv.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/nativeconv.mli') diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 4dddb9fd30..abc9e3a3ca 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -11,7 +11,7 @@ open Nativelambda (** This module implements the conversion test by compiling to OCaml code *) -val native_conv : conv_pb -> evars -> types conversion_function +val native_conv : conv_pb -> evars -> 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/nativeconv.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/nativeconv.mli') diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 4dddb9fd30..6c0b310cbf 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*