diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declaremods.ml | 26 | ||||
-rw-r--r-- | library/declaremods.mli | 27 |
2 files changed, 2 insertions, 51 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 356defcac..e6224d68a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -16,16 +16,7 @@ open Libnames open Libobject open Lib open Mod_subst - -(** Rigid / flexible signature *) - -type 'a module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - -(** Should we adapt a few scopes during functor application ? *) - -type scope_subst = (string * string) list +open Vernacexpr let scope_subst = ref (String.Map.empty : string String.Map.t) @@ -41,14 +32,6 @@ let subst_scope sc = let reset_scope_subst () = scope_subst := String.Map.empty -(** Which 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 @@ -56,15 +39,8 @@ let inl2intopt = function | InlineAt i -> Some i | DefaultInline -> default_inline () -type funct_app_annot = - { ann_inline : inline; - ann_scope_subst : scope_subst } - let inline_annot a = inl2intopt a.ann_inline -type 'a annotated = ('a * funct_app_annot) - - (* modules and components *) (* OBSOLETE This type is a functional closure of substitutive lib_objects. diff --git a/library/declaremods.mli b/library/declaremods.mli index d7121d6f6..e350c9fb1 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -14,38 +14,13 @@ open Environ open Libnames open Libobject open Lib +open Vernacexpr (** This modules provides official functions to declare modules and module types *) -(** Rigid / flexible signature *) - -type 'a module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - -(** Should we adapt a few scopes during functor application ? *) - -type scope_subst = (string * string) list - val subst_scope : string -> string -(** Which 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 - -(** The type of annotations for functor applications *) - -type funct_app_annot = - { ann_inline : inline; - ann_scope_subst : scope_subst } - -type 'a annotated = ('a * funct_app_annot) - (** {6 Modules } *) (** [declare_module interp_modtype interp_modexpr id fargs typ expr] |