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

1 files changed, 36 insertions, 7 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index cb6b74bcc9..49467a393e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -12,7 +12,6 @@ open Names
 open Tacexpr
 open Misctypes
 open Constrexpr
-open Notation_term
 open Decl_kinds
 open Libnames
 
@@ -26,6 +25,7 @@ type lreference = reference
 type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
 
 type goal_identifier = string
+type scope_name = string
 
 type goal_reference =
   | OpenSubgoals
@@ -179,9 +179,6 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
-type module_ast_inl = module_ast Declaremods.annotated
-type module_binder = bool option * lident list * module_ast_inl
-
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
   | TacNonTerm of Loc.t * string * (Names.Id.t * string) option
@@ -203,13 +200,45 @@ type scheme =
   | CaseScheme of bool * reference or_by_notation * sort_expr
   | EqualityScheme of reference or_by_notation
 
-type inline = int option (* inlining level, none for no inlining *)
-
 type bullet =
     | Dash
     | Star
     | Plus
 
+(** {6 Types concerning the module layer} *)
+
+(** 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
+
+(** Should we adapt a few scopes during functor application ? *)
+
+type scope_subst = (string * string) list
+
+(** 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)
+
+type module_ast_inl = module_ast annotated
+type module_binder = bool option * lident list * module_ast_inl
+
+(** {6 The type of vernacular expressions} *)
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -277,7 +306,7 @@ type vernac_expr =
   | VernacDeclareModule of bool option * lident *
       module_binder list * module_ast_inl
   | VernacDefineModule of bool option * lident * module_binder list *
-      module_ast_inl Declaremods.module_signature * module_ast_inl list
+      module_ast_inl module_signature * module_ast_inl list
   | VernacDeclareModuleType of lident *
       module_binder list * module_ast_inl list * module_ast_inl list
   | VernacInclude of module_ast_inl list