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, 9 insertions, 3 deletions

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f634719f9a..b6b6b48287 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -14,14 +14,20 @@ open Declarations
 
 (** The type of environments. *)
 
+type link_info =
+  | Linked of string * bool
+  | LinkedInteractive of string * bool
+  | NotLinked
 
 type key = int option ref
 
-type constant_key = constant_body * key
+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}
 
@@ -77,5 +83,5 @@ val lookup_constant_key : constant -> env -> constant_key
 val lookup_constant : constant -> env -> constant_body
 
 (** Mutual Inductives *)
+val lookup_mind_key : mutual_inductive -> env -> mind_key
 val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
-