diff options
| author | Pierre-Marie Pédrot | 2020-11-09 18:26:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-12 13:59:22 +0100 |
| commit | 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 (patch) | |
| tree | 258650a01e5925b1e344662df220e7c371f6584f /kernel/environ.ml | |
| parent | c12471f1c5192ba1f18adac2109913c7b55ae50b (diff) | |
Merge the Linked and LinkedInteractive constructors.
There was not any difference between those after the cleanup patches that
come before.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 914c951eb6..5914e66fc3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref type link_info = | Linked of string - | LinkedInteractive of string | NotLinked type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) |