From 79b6291ccda61f631aa2cfec9a12d6ea2a34fa96 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 13 Mar 2013 18:01:16 +0000
Subject: 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
---
 library/declaremods.ml  | 26 +-------------------------
 library/declaremods.mli | 27 +--------------------------
 2 files changed, 2 insertions(+), 51 deletions(-)

(limited to 'library')

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]
-- 
cgit v1.2.3