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.

1 files changed, 4 insertions, 4 deletions

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index c5417b2b6..947e0a148 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,11 +373,11 @@ let makeblock env cn tag args =
 
 (* Translation of constants *)
 
-let rec get_allias env kn =
+let rec get_allias env (kn, u as p) =
   let tps = (lookup_constant kn env).const_body_code in
   match Cemitcodes.force tps with
   |  Cemitcodes.BCallias kn' -> get_allias env kn'
-  | _ -> kn
+  | _ -> p
 
 (*i Global environment *)
 
@@ -647,8 +647,8 @@ let rec lambda_of_constr env sigma c =
 
 and lambda_of_app env sigma f args =
   match kind_of_term f with
-  | Const (kn,u) ->
-      let kn = get_allias !global_env kn in
+  | Const (kn,u as c) ->
+      let kn,u = get_allias !global_env c in
       let cb = lookup_constant kn !global_env in
       (try
           let prefix = get_const_prefix !global_env kn in