From 381b2c6e77cd204aa143192a5a65e8832ae0633b Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Sun, 29 Dec 2013 10:53:06 -0500
Subject: Got rid of unused lazy flag in the native compiler.

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

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 7e46a0550..800c8e5fb 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -14,7 +14,6 @@ open Pre_env
 open Nativevalues
 
 (** This file defines the lambda code generation phase of the native compiler *)
-      
 type lambda =
   | Lrel          of name * int 
   | Lvar          of identifier
@@ -90,15 +89,15 @@ let get_mind_prefix env mind =
    let _,name = lookup_mind_key mind env in
    match !name with
    | NotLinked -> ""
-   | Linked (s,_) -> s
-   | LinkedInteractive (s,_) -> s
+   | Linked s -> s
+   | LinkedInteractive s -> s
 
 let get_const_prefix env c =
    let _,(nameref,_) = lookup_constant_key c env in
    match !nameref with
    | NotLinked -> ""
-   | Linked (s,_) -> s
-   | LinkedInteractive (s,_) -> s
+   | Linked s -> s
+   | LinkedInteractive s -> s
     
 (* A generic map function *)
 
-- 
cgit v1.2.3