diff options
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 8 |
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 |