From c87579a20b8f99b8dd968320f96dd470d274c3ca 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/cbytegen.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cbytegen.mli')

diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index d0bfd46c00..eab36d8b24 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -13,7 +13,7 @@ val compile_constant_body : env -> constant_def -> body_code
 
 (** Shortcut of the previous function used during module strengthening *)
 
-val compile_alias : constant -> body_code
+val compile_alias : pconstant -> body_code
 
 (** spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
@@ -33,7 +33,7 @@ val dynamic_int31_compilation : bool -> comp_env ->
            works as follow: checks if all the arguments are non-pointers
            if they are applies the operation (second argument) if not
            all of them are, returns to a coq definition (third argument) *)
-val op_compilation : int -> instruction -> constant -> bool -> comp_env ->
+val op_compilation : int -> instruction -> pconstant -> bool -> comp_env ->
                              constr array -> int -> bytecodes-> bytecodes
 
 (*spiwack: compiling function to insert dynamic decompilation before
-- 
cgit v1.2.3