From 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2020 18:26:21 +0100
Subject: Merge the Linked and LinkedInteractive constructors.

There was not any difference between those after the cleanup patches that
come before.
---
 kernel/nativelambda.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/nativelambda.ml')

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 *)
 
-- 
cgit v1.2.3