From 8309a98096facfba448c9d8d298ba3903145831a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 15 Jan 2015 18:45:27 +0530 Subject: Correct restriction of vm_compute when handling universe polymorphic definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions. --- kernel/conv_oracle.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel/conv_oracle.mli') diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 550076782..629912220 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -16,7 +16,8 @@ val empty : oracle If [oracle_order kn1 kn2] is true, then unfold kn1 first. Note: the oracle does not introduce incompleteness, it only tries to postpone unfolding of "opaque" constants. *) -val oracle_order : oracle -> bool -> constant tableKey -> constant tableKey -> bool +val oracle_order : ('a -> constant) -> oracle -> bool -> + 'a tableKey -> 'a tableKey -> bool (** Priority for the expansion of constant in the conversion test. * Higher levels means that the expansion is less prioritary. -- cgit v1.2.3