Got rid of unused lazy flag in the native compiler.

4 files changed, 18 insertions, 20 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 219ccd220..4e34cd60f 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1170,7 +1170,7 @@ let string_of_dirpath s = "N"^string_of_dirpath s
 let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir)
 
 let link_info_of_dirpath dir =
-  ref (Linked (mod_uid_of_dirpath dir ^ ".", false))
+  ref (Linked (mod_uid_of_dirpath dir ^ "."))
 
 let string_of_name x =
   match x with
@@ -1487,8 +1487,8 @@ let compile_constant env prefix ~interactive con body =
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
-        if interactive then LinkedInteractive (prefix, is_lazy)
-        else Linked (prefix, is_lazy)
+        if interactive then LinkedInteractive prefix
+        else Linked prefix
       in
       let l = con_label con in
       let auxdefs,code = compile_with_fv env [] (Some l) code in
@@ -1499,8 +1499,8 @@ let compile_constant env prefix ~interactive con body =
   | _ -> 
       let i = push_symbol (SymbConst con) in
       [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))],
-      if interactive then LinkedInteractive (prefix, false)
-      else Linked (prefix, false)
+      if interactive then LinkedInteractive prefix
+      else Linked prefix
 
 let loaded_native_files = ref ([] : string list)
 
@@ -1513,10 +1513,10 @@ let register_native_file s =
 let is_code_loaded ~interactive name =
   match !name with
   | NotLinked -> false
-  | LinkedInteractive (s,_) ->
+  | LinkedInteractive s ->
       if (interactive && is_loaded_native_file s) then true
       else (name := NotLinked; false)
-  | Linked (s,_) ->
+  | Linked s ->
       if is_loaded_native_file s then true
       else (name := NotLinked; false)
 
@@ -1565,8 +1565,8 @@ let compile_mind_deps env prefix ~interactive
       compile_mind prefix ~interactive mib mind comp_stack
     in
     let name =
-      if interactive then LinkedInteractive (prefix, false)
-      else Linked (prefix, false)
+      if interactive then LinkedInteractive prefix
+      else Linked prefix
     in
     let upd = (nameref, name) in
     let mind_updates = Mindmap_env.add mind upd mind_updates in
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 *)
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index d96492020..64d9d1a17 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -27,12 +27,11 @@ open Declarations
 (* used by the VM. *)
 type key = int option ref
 
-(** Linking information for the native compiler. The boolean flag indicates if
-  the term is protected by a lazy tag. *)
+(** Linking information for the native compiler. *)
 
 type link_info =
-  | Linked of string * bool
-  | LinkedInteractive of string * bool
+  | Linked of string
+  | LinkedInteractive of string
   | NotLinked
 
 type constant_key = constant_body * (link_info ref * key)
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index b6b6b4828..93c8b15f7 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -15,8 +15,8 @@ open Declarations
 (** The type of environments. *)
 
 type link_info =
-  | Linked of string * bool
-  | LinkedInteractive of string * bool
+  | Linked of string
+  | LinkedInteractive of string
   | NotLinked
 
 type key = int option ref