diff options
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index e98e97907a..18f16f427d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -111,14 +111,12 @@ let get_mind_prefix env mind = match !name with | NotLinked -> "" | Linked s -> s - | LinkedInteractive s -> s let get_const_prefix env c = let _,(nameref,_) = lookup_constant_key c env in match !nameref with | NotLinked -> "" | Linked s -> s - | LinkedInteractive s -> s (* A generic map function *) |