Removing native_name reference from constant_body.

For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.

1 files changed, 18 insertions, 4 deletions

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index e543c4e687..d96492020a 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -22,14 +22,26 @@ open Declarations
 
 (* The type of environments. *)
 
-
+(* The key attached to each constant is used by the VM to retrieve previous *)
+(* evaluations of the constant. It is essentially an index in the symbols table *)
+(* used by the VM. *)
 type key = int option ref
 
-type constant_key = constant_body * key
+(** Linking information for the native compiler. The boolean flag indicates if
+  the term is protected by a lazy tag. *)
+
+type link_info =
+  | Linked of string * bool
+  | LinkedInteractive of string * bool
+  | NotLinked
+
+type constant_key = constant_body * (link_info ref * key)
+
+type mind_key = mutual_inductive_body * link_info ref
 
 type globals = {
   env_constants : constant_key Cmap_env.t;
-  env_inductives : mutual_inductive_body Mindmap_env.t;
+  env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
@@ -139,5 +151,7 @@ let lookup_constant kn env =
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  Mindmap_env.find kn env.env_globals.env_inductives
+  fst (Mindmap_env.find kn env.env_globals.env_inductives)
 
+let lookup_mind_key kn env =
+  Mindmap_env.find kn env.env_globals.env_inductives