diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 18:01:16 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 18:01:16 +0000 |
commit | 79b6291ccda61f631aa2cfec9a12d6ea2a34fa96 (patch) | |
tree | 1c0462389248e1ecb4a9071add18c87d9648c6f1 /library/declaremods.mli | |
parent | a74338cc598b5fb45e2cc148d243433500bb5294 (diff) |
Modules and ppvernac, sequel of Enrico's commit 16261
After some investigation, I see no reason to try to hack
the nametab in ppvernac, since everything happens there
at a lower level (constr_expr). So the offending code that
Enrico protected with a State.with_state_protection is now gone.
By the way, moved some types from Declaremods to Vernacexpr
to avoid some dependencies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.mli')
-rw-r--r-- | library/declaremods.mli | 27 |
1 files changed, 1 insertions, 26 deletions
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] |