diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 752fdd793..f0f273f35 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -158,6 +158,10 @@ val add_module_parameter : MBId.t -> Entries.module_struct_entry -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer +(** Traditional mode: check at end of module that no future was + created. *) +val allow_delayed_constants : bool ref + (** The optional result type is given without its functorial part *) val end_module : |