summaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
commit0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch)
tree12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /kernel/nativelambda.ml
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r--kernel/nativelambda.ml9
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 543397df..383f8102 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -375,9 +375,12 @@ let makeblock env cn u tag args =
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'
- | _ -> p
+ match tps with
+ | None -> p
+ | Some tps ->
+ match Cemitcodes.force tps with
+ | Cemitcodes.BCallias kn' -> get_allias env kn'
+ | _ -> p
(*i Global environment *)