diff options
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 8 |
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 |