diff options
| author | coqbot-app[bot] | 2020-11-13 15:28:53 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-13 15:28:53 +0000 |
| commit | 9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (patch) | |
| tree | 0feb6d52dff924f53d5f39d824816f0ee77e50e5 /kernel/nativelambda.ml | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
| parent | 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 (diff) | |
Merge PR #13358: Merge the Linked / LinkedInteractive native link information constructors
Reviewed-by: SkySkimmer
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 *) |