From d3eac3d5fc8e5af499eb8750ca08ead8562dac6f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 28 Dec 2013 20:39:17 -0500 Subject: 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. --- kernel/nativelambda.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/nativelambda.ml') 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 -- cgit v1.2.3