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

(limited to 'kernel/cemitcodes.mli')

diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 287c393046..cec9013060 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of constant
+  | Reloc_getglobal of constant Univ.puniverses
 
 type patch = reloc_info * int
 
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of constant
+  | BCallias of constant Univ.puniverses
   | BCconstant
 
 
-- 
cgit v1.2.3