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/nativelambda.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/nativelambda.ml') 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 -- cgit v1.2.3