diff options
| author | Maxime Dénès | 2013-12-29 10:53:06 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2013-12-29 11:04:25 -0500 |
| commit | 381b2c6e77cd204aa143192a5a65e8832ae0633b (patch) | |
| tree | 2f26dca0d8085664d9bffde2c0dde5939c456b84 /kernel/pre_env.ml | |
| parent | 651094ccfd2d8106a8b0e75c27dc89afb369d4b3 (diff) | |
Got rid of unused lazy flag in the native compiler.
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) |