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/environ.mli | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
| parent | 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 (diff) | |
Merge PR #13358: Merge the Linked / LinkedInteractive native link information constructors
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 60696184ef..6d0ca93707 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -37,7 +37,6 @@ val dummy_lazy_val : unit -> lazy_val (** Linking information for the native compiler *) type link_info = | Linked of string - | LinkedInteractive of string | NotLinked type key = int CEphemeron.key option ref |