diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index b6b6b48287..93c8b15f76 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -15,8 +15,8 @@ open Declarations (** The type of environments. *) type link_info = - | Linked of string * bool - | LinkedInteractive of string * bool + | Linked of string + | LinkedInteractive of string | NotLinked type key = int option ref |