diff options
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r-- | library/declaremods.ml | 16 |
1 files changed, 15 insertions, 1 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 |