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, 4 insertions, 4 deletions

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index cfb128d50..7e46a0550 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -87,15 +87,15 @@ let shift subst = subs_shft (1, subst)
 
 (* Linked code location utilities *)
 let get_mind_prefix env mind =
-   let mib = lookup_mind mind env in
-   match !(mib.mind_native_name) with
+   let _,name = lookup_mind_key mind env in
+   match !name with
    | NotLinked -> ""
    | Linked (s,_) -> s
    | LinkedInteractive (s,_) -> s
 
 let get_const_prefix env c =
-   let cb = lookup_constant c env in
-   match !(cb.const_native_name) with
+   let _,(nameref,_) = lookup_constant_key c env in
+   match !nameref with
    | NotLinked -> ""
    | Linked (s,_) -> s
    | LinkedInteractive (s,_) -> s