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/nativecode.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 433e2c5055..66577fecc4 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1772,7 +1772,7 @@ let compile_constant env sigma prefix ~interactive con cb =
   match cb.const_proj with
   | None ->
     begin match cb.const_body with
-    | Def t ->
+    | Def t when not cb.const_polymorphic ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
       if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
@@ -1902,8 +1902,8 @@ let compile_mind_deps env prefix ~interactive
 let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
-  | Const (c,u) ->
-      let c = get_allias env c in
+  | Const c ->
+      let c,u = get_allias env c in
       let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
       if is_code_loaded ~interactive nameref
-- 
cgit v1.2.3