From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 kernel/nativelambda.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'kernel/nativelambda.ml')

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 *)
 
-- 
cgit v1.2.3