diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-23 16:19:43 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-23 16:19:43 +0200 |
commit | 5c34cfa54ec1959758baa3dd283e2e30853380db (patch) | |
tree | be7c3a478307fc000f04e55f34e670d4dafcc451 /library | |
parent | d8532c76d8e758f95a5dcc36e0c9bc5fd144be16 (diff) | |
parent | 79ff2bc044aa86a5ce30f0c24647db8c8e2544fa (diff) |
Merge PR #7152: [api] Remove dependency of library on Vernacexpr.
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 |