diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 24572da59..43b908e1f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -40,10 +40,12 @@ type constant_def = | Def of Lazyconstr.constr_substituted | OpaqueDef of Lazyconstr.lazy_constr +(** Linking information for the native compiler. The boolean flag indicates if + the term is protected by a lazy tag *) + type native_name = - | Linked of string - | LinkedLazy of string - | LinkedInteractive of string + | Linked of string * bool + | LinkedInteractive of string * bool | NotLinked type constant_body = { |