diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declaremods.ml | 16 | ||||
-rw-r--r-- | library/declaremods.mli | 16 |
2 files changed, 30 insertions, 2 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 762efc5e3..1d5df49cf 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,11 +17,25 @@ open Entries open Libnames open Libobject open Mod_subst -open Vernacexpr open Misctypes (** {6 Inlining levels} *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function diff --git a/library/declaremods.mli b/library/declaremods.mli index fd8d29614..4aee7feae 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -9,10 +9,24 @@ (************************************************************************) open Names -open Vernacexpr (** {6 Modules } *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + type 'modast module_interpretor = Environ.env -> Misctypes.module_kind -> 'modast -> Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t |