diff options
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index d96492020a..64d9d1a171 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -27,12 +27,11 @@ open Declarations (* used by the VM. *) type key = int option ref -(** Linking information for the native compiler. The boolean flag indicates if - the term is protected by a lazy tag. *) +(** Linking information for the native compiler. *) type link_info = - | Linked of string * bool - | LinkedInteractive of string * bool + | Linked of string + | LinkedInteractive of string | NotLinked type constant_key = constant_body * (link_info ref * key) |