Imported Upstream version 8.5~beta1+dfsg

1 files changed, 746 insertions, 848 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 6b33e4b7..cc7c4d7f 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1,53 +1,24 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Declarations
 open Entries
 open Libnames
 open Libobject
-open Lib
-open Nametab
 open Mod_subst
+open Vernacexpr
+open Misctypes
 
-(** 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
-
-let scope_subst = ref (Stringmap.empty : string Stringmap.t)
-
-let add_scope_subst sc sc' =
-  scope_subst := Stringmap.add sc sc' !scope_subst
-
-let register_scope_subst scl =
-  List.iter (fun (sc1,sc2) -> add_scope_subst sc1 sc2) scl
-
-let subst_scope sc =
- try Stringmap.find sc !scope_subst with Not_found -> sc
-
-let reset_scope_subst () =
-  scope_subst := Stringmap.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
+(** {6 Inlining levels} *)
 
 let default_inline () = Some (Flags.get_inline_level ())
 
@@ -56,57 +27,93 @@ let inl2intopt = function
   | InlineAt i -> Some i
   | DefaultInline -> default_inline ()
 
-type funct_app_annot =
-  { ann_inline : inline;
-    ann_scope_subst : scope_subst }
+(** {6 Substitutive objects}
 
-let inline_annot a = inl2intopt a.ann_inline
+   - The list of bound identifiers is nonempty only if the objects
+     are owned by a functor
 
-type 'a annotated = ('a * funct_app_annot)
+   - Then comes either the object segment itself (for interactive
+     modules), or a compact way to store derived objects (path to
+     a earlier module + subtitution).
+*)
 
+type algebraic_objects =
+  | Objs of Lib.lib_objects
+  | Ref of module_path * substitution
 
-(* modules and components *)
+type substitutive_objects = MBId.t list * algebraic_objects
 
-(* OBSOLETE This type is a functional closure of substitutive lib_objects.
+(** ModSubstObjs : a cache of module substitutive objects
 
-   The first part is a partial substitution (which will be later
-   applied to lib_objects when completed).
+   This table is common to modules and module types.
+   -  For a Module M:=N, the objects of N will be reloaded
+      with M after substitution.
+   -  For a Module M:SIG:=..., the module M gets its objects from SIG
 
-   The second one is a list of bound identifiers which is nonempty
-   only if the objects are owned by a fuctor
+   Invariants:
+   - A alias (i.e. a module path inside a Ref constructor) should
+     never lead to another alias, but rather to a concrete Objs
+     constructor.
 
-   The third one is the "self" ident of the signature (or structure),
-   which should be substituted in lib_objects with the real name of
-   the module.
+   We will plug later a handler dealing with missing entries in the
+   cache. Such missing entries may come from inner parts of module
+   types, which aren't registered by the standard libobject machinery.
+*)
 
-   The fourth one is the segment itself which can contain references
-   to identifiers in the domain of the substitution or in other two
-   parts. These references are invalid in the current scope and
-   therefore must be substitued with valid names before use.
+module ModSubstObjs :
+ sig
+   val set : module_path -> substitutive_objects -> unit
+   val get : module_path -> substitutive_objects
+   val set_missing_handler : (module_path -> substitutive_objects) -> unit
+ end =
+ struct
+   let table =
+     Summary.ref (MPmap.empty : substitutive_objects MPmap.t)
+       ~name:"MODULE-SUBSTOBJS"
+   let missing_handler = ref (fun mp -> assert false)
+   let set_missing_handler f = (missing_handler := f)
+   let set mp objs = (table := MPmap.add mp objs !table)
+   let get mp =
+     try MPmap.find mp !table with Not_found -> !missing_handler mp
+ end
 
-*)
-type substitutive_objects =
-     mod_bound_id list * module_path * lib_objects
+(** Some utilities about substitutive objects :
+    substitution, expansion *)
+
+let sobjs_no_functor (mbids,_) = List.is_empty mbids
+
+let subst_aobjs sub = function
+  | Objs o -> Objs (Lib.subst_objects sub o)
+  | Ref (mp, sub0) -> Ref (mp, join sub0 sub)
+
+let subst_sobjs sub (mbids,aobjs) = (mbids, subst_aobjs sub aobjs)
+
+let expand_aobjs = function
+  | Objs o -> o
+  | Ref (mp, sub) ->
+    match ModSubstObjs.get mp with
+      | (_,Objs o) -> Lib.subst_objects sub o
+      | _ -> assert false (* Invariant : any alias points to concrete objs *)
 
+let expand_sobjs (_,aobjs) = expand_aobjs aobjs
 
-(* For each module, we store the following things:
 
-   In modtab_substobjs: substitutive_objects
-     when we will do Module M:=N, the objects of N will be reloaded
-     with M after substitution
+(** {6 ModObjs : a cache of module objects}
 
-   In modtab_objects: "substituted objects" @ "keep objects"
+   For each module, we also store a cache of
+   "prefix", "substituted objects", "keep objects".
+   This is used for instance to implement the "Import" command.
 
-   substituted objects -
+   substituted objects :
      roughly the objects above after the substitution - we need to
      keep them to call open_object when the module is opened (imported)
 
-   keep objects -
+   keep objects :
      The list of non-substitutive objects - as above, for each of
      them we will call open_object when the module is opened
 
    (Some) Invariants:
-   * If the module is a functor, the two latter lists are empty.
+   * If the module is a functor, it won't appear in this cache.
 
    * Module objects in substitutive_objects part have empty substituted
      objects.
@@ -114,190 +121,88 @@ type substitutive_objects =
    * Modules which where created with Module M:=mexpr or with
      Module M:SIG. ... End M. have the keep list empty.
 *)
-let modtab_substobjs =
-  ref (MPmap.empty : substitutive_objects MPmap.t)
-let modtab_objects =
-  ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
-
-
-(* currently started interactive module (if any) - its arguments (if it
-   is a functor) and declared output type *)
-let openmod_info =
-  ref ((MPfile(initial_dir),[],None,[])
-	 : module_path *  mod_bound_id list *
-           (module_struct_entry * int option) option *
-	   module_type_body list)
-
-(* The library_cache here is needed to avoid recalculations of
-   substituted modules object during "reloading" of libraries *)
-let library_cache = ref Dirmap.empty
-
-let _ = Summary.declare_summary "MODULE-INFO"
-	  { Summary.freeze_function = (fun () ->
-					 !modtab_substobjs,
-					 !modtab_objects,
-					 !openmod_info,
-					 !library_cache);
-	    Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) ->
-					   modtab_substobjs := sobjs;
-					   modtab_objects := objs;
-					   openmod_info := info;
-					   library_cache := libcache);
-	    Summary.init_function = (fun () ->
-				       modtab_substobjs := MPmap.empty;
-				       modtab_objects := MPmap.empty;
-				       openmod_info := ((MPfile(initial_dir),
-							 [],None,[]));
-				       library_cache := Dirmap.empty) }
-
-(* auxiliary functions to transform full_path and kernel_name given
-   by Lib into module_path and dir_path needed for modules *)
 
-let mp_of_kn kn =
-  let mp,sec,l = repr_kn kn in
-    if sec=empty_dirpath then
-      MPdot (mp,l)
-    else
-      anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
-
-let dir_of_sp sp =
-  let dir,id = repr_path sp in
-    add_dirpath_suffix dir id
-
-(* Subtyping checks *)
-
-let check_sub mtb sub_mtb_l =
-  (* The constraints are checked and forgot immediately : *)
-  ignore (List.fold_right
-	    (fun sub_mtb env ->
-	       Environ.add_constraints
-		 (Subtyping.check_subtypes env mtb sub_mtb) env)
-	    sub_mtb_l (Global.env()))
+type module_objects = object_prefix * Lib.lib_objects * Lib.lib_objects
 
-(* This function checks if the type calculated for the module [mp] is
-   a subtype of all signatures in [sub_mtb_l]. Uses only the global
-   environment. *)
-
-let check_subtypes mp sub_mtb_l =
-  let mb =
-    try Global.lookup_module mp
-    with Not_found -> assert false
-  in
-  let mtb = Modops.module_type_of_module None mb in
-  check_sub mtb sub_mtb_l
+module ModObjs :
+ sig
+   val set : module_path -> module_objects -> unit
+   val get : module_path -> module_objects (* may raise Not_found *)
+   val all : unit -> module_objects MPmap.t
+ end =
+ struct
+   let table =
+     Summary.ref (MPmap.empty : module_objects MPmap.t)
+       ~name:"MODULE-OBJS"
+   let set mp objs = (table := MPmap.add mp objs !table)
+   let get mp = MPmap.find mp !table
+   let all () = !table
+ end
 
-(* Same for module type [mp] *)
 
-let check_subtypes_mt mp sub_mtb_l =
-  let mtb =
-    try Global.lookup_modtype mp
-    with Not_found -> assert false
-  in
-  check_sub mtb sub_mtb_l
+(** {6 Name management}
 
-(* Create a functor type entry *)
+    Auxiliary functions to transform full_path and kernel_name given
+    by Lib into module_path and DirPath.t needed for modules
+*)
 
-let funct_entry args m =
-  List.fold_right
-    (fun (arg_id,(arg_t,_)) mte -> MSEfunctor (arg_id,arg_t,mte))
-    args m
+let mp_of_kn kn =
+  let mp,sec,l = repr_kn kn in
+  assert (DirPath.is_empty sec);
+  MPdot (mp,l)
 
-(* Prepare the module type list for check of subtypes *)
+let dir_of_sp sp =
+  let dir,id = repr_path sp in
+  add_dirpath_suffix dir id
 
-let build_subtypes interp_modtype mp args mtys =
-  List.map
-    (fun (m,ann) ->
-       let inl = inline_annot ann in
-       let mte = interp_modtype (Global.env()) m in
-       let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in
-       let funct_mtb =
-	 List.fold_right
-           (fun (arg_id,(arg_t,arg_inl)) mte ->
-              let arg_t =
-		Mod_typing.translate_module_type (Global.env())
-		  (MPbound arg_id) arg_inl arg_t
-	      in
-              SEBfunctor(arg_id,arg_t,mte))
-           args mtb.typ_expr
-       in
-       { mtb with typ_expr = funct_mtb })
-    mtys
 
+(** {6 Declaration of module substitutive objects} *)
 
-(* These functions register the visibility of the module and iterates
-   through its components. They are called by plenty module functions *)
+(** These functions register the visibility of the module and iterates
+    through its components. They are called by plenty of module functions *)
 
-let compute_visibility exists what i dir dirinfo =
+let consistency_checks exists dir dirinfo =
   if exists then
-    if
-      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
-      with Not_found -> false
-    then
-      Nametab.Exactly i
-    else
-      errorlabstrm (what^"_module")
-	(pr_dirpath dir ++ str " should already exist!")
+    let globref =
+      try Nametab.locate_dir (qualid_of_dirpath dir)
+      with Not_found ->
+        anomaly (pr_dirpath dir ++ str " should already exist!")
+    in
+    assert (eq_global_dir_reference globref dirinfo)
   else
     if Nametab.exists_dir dir then
-      errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
-    else
-      Nametab.Until i
-(*
-let do_load_and_subst_module i dir mp substobjs keep =
-  let prefix = (dir,(mp,empty_dirpath)) in
-  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = compute_visibility false "load_and_subst" i dir dirinfo in
-  let objects = compute_subst_objects mp substobjs resolver in
-  Nametab.push_dir vis dir dirinfo;
-  modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
-  match objects with
-  | Some (subst,seg) ->
-      let seg = load_and_subst_objects (i+1) prefix subst seg in
-      modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
-      load_objects (i+1) prefix keep;
-      Some (seg@keep)
-  | None ->
-      None
-*)
-
-let do_module exists what iter_objects i dir mp substobjs keep=
-  let prefix = (dir,(mp,empty_dirpath)) in
-  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = compute_visibility exists what i dir dirinfo in
-    Nametab.push_dir vis dir dirinfo;
-    modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
-    match substobjs with
-	([],mp1,objs) -> 
-	  modtab_objects := MPmap.add mp (prefix,objs@keep) !modtab_objects;
-	  iter_objects (i+1) prefix (objs@keep)  
-      | (mbids,_,_) ->  ()
-
-let conv_names_do_module exists what iter_objects i
-      (sp,kn) substobjs =
-  let dir,mp = dir_of_sp sp, mp_of_kn kn in
-  do_module exists what iter_objects i dir mp substobjs []
-
-(* Interactive modules and module types cannot be recached! cache_mod*
-   functions can be called only once (and "end_mod*" set the flag to
-   false then)
-*)
-let cache_module ((sp,kn),substobjs) =
-  let dir,mp = dir_of_sp sp, mp_of_kn kn in
-    do_module false "cache" load_objects 1 dir mp substobjs []
-
-(* When this function is called the module itself is already in the
-   environment. This function loads its objects only *)
-
-let load_module i (oname,substobjs) =
-  conv_names_do_module false "load" load_objects i oname substobjs
-
-let open_module i (oname,substobjs) =
-  conv_names_do_module true "open" open_objects i oname substobjs
-
-let subst_module (subst,(mbids,mp,objs)) =
-  (mbids,subst_mp subst mp, subst_objects subst objs)
-
-let classify_module substobjs = Substitute substobjs
+      anomaly (pr_dirpath dir ++ str " already exists")
+
+let compute_visibility exists i =
+  if exists then Nametab.Exactly i else Nametab.Until i
+
+(** Iterate some function [iter_objects] on all components of a module *)
+
+let do_module exists iter_objects i dir mp sobjs kobjs =
+  let prefix = (dir,(mp,DirPath.empty)) in
+  let dirinfo = DirModule prefix in
+  consistency_checks exists dir dirinfo;
+  Nametab.push_dir (compute_visibility exists i) dir dirinfo;
+  ModSubstObjs.set mp sobjs;
+  (* If we're not a functor, let's iter on the internal components *)
+  if sobjs_no_functor sobjs then begin
+    let objs = expand_sobjs sobjs in
+    ModObjs.set mp (prefix,objs,kobjs);
+    iter_objects (i+1) prefix objs;
+    iter_objects (i+1) prefix kobjs
+  end
+
+let do_module' exists iter_objects i ((sp,kn),sobjs) =
+  do_module exists iter_objects i (dir_of_sp sp) (mp_of_kn kn) sobjs []
+
+(** Nota: Interactive modules and module types cannot be recached!
+    This used to be checked here via a flag along the substobjs. *)
+
+let cache_module = do_module' false Lib.load_objects 1
+let load_module = do_module' false Lib.load_objects
+let open_module = do_module' true Lib.open_objects
+let subst_module (subst,sobjs) = subst_sobjs subst sobjs
+let classify_module sobjs = Substitute sobjs
 
 let (in_module : substitutive_objects -> obj),
     (out_module : obj -> substitutive_objects) =
@@ -308,755 +213,748 @@ let (in_module : substitutive_objects -> obj),
     subst_function = subst_module;
     classify_function = classify_module }
 
-let cache_keep _ = anomaly "This module should not be cached!"
 
-let load_keep i ((sp,kn),seg) =
-  let mp = mp_of_kn kn in
-  let prefix = dir_of_sp sp, (mp,empty_dirpath) in
-    begin
-      try
-	let prefix',objects = MPmap.find mp !modtab_objects in
-	  if prefix' <> prefix then
-	    anomaly "Two different modules with the same path!";
-	  modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects;
-      with
-	  Not_found -> anomaly "Keep objects before substitutive"
-    end;
-    load_objects i prefix seg
-
-let open_keep i ((sp,kn),seg) =
-  let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
-    open_objects i (dirpath,(mp,empty_dirpath)) seg
-
-let in_modkeep : lib_objects -> obj =
-  declare_object {(default_object "MODULE KEEP OBJECTS") with
+(** {6 Declaration of module keep objects} *)
+
+let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
+
+let load_keep i ((sp,kn),kobjs) =
+  (* Invariant : seg isn't empty *)
+  let dir = dir_of_sp sp and mp = mp_of_kn kn in
+  let prefix = (dir,(mp,DirPath.empty)) in
+  let prefix',sobjs,kobjs0 =
+    try ModObjs.get mp
+    with Not_found -> assert false (* a substobjs should already be loaded *)
+  in
+  assert (eq_op prefix' prefix);
+  assert (List.is_empty kobjs0);
+  ModObjs.set mp (prefix,sobjs,kobjs);
+  Lib.load_objects i prefix kobjs
+
+let open_keep i ((sp,kn),kobjs) =
+  let dir = dir_of_sp sp and mp = mp_of_kn kn in
+  let prefix = (dir,(mp,DirPath.empty)) in
+  Lib.open_objects i prefix kobjs
+
+let in_modkeep : Lib.lib_objects -> obj =
+  declare_object {(default_object "MODULE KEEP") with
     cache_function = cache_keep;
     load_function = load_keep;
     open_function = open_keep }
 
-(* we remember objects for a module type. In case of a declaration:
-   Module M:SIG:=...
-   The module M gets its objects from SIG
-*)
-let modtypetab =
-  ref (MPmap.empty : substitutive_objects MPmap.t)
 
-(* currently started interactive module type. We remember its arguments
-   if it is a functor type *)
-let openmodtype_info =
-  ref ([],[] : mod_bound_id list * module_type_body list)
+(** {6 Declaration of module type substitutive objects} *)
 
-let _ = Summary.declare_summary "MODTYPE-INFO"
-	  { Summary.freeze_function = (fun () ->
-					 !modtypetab,!openmodtype_info);
-	    Summary.unfreeze_function = (fun ft ->
-					   modtypetab := fst ft;
-					   openmodtype_info := snd ft);
-	    Summary.init_function = (fun () ->
-				       modtypetab := MPmap.empty;
-				       openmodtype_info := [],[]) }
+(** Nota: Interactive modules and module types cannot be recached!
+    This used to be checked more properly here. *)
 
+let do_modtype i sp mp sobjs =
+  if Nametab.exists_modtype sp then
+    anomaly (pr_path sp ++ str " already exists");
+  Nametab.push_modtype (Nametab.Until i) sp mp;
+  ModSubstObjs.set mp sobjs
 
-let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
-  let mp = mp_of_kn kn in
+let cache_modtype ((sp,kn),sobjs) = do_modtype 1 sp (mp_of_kn kn) sobjs
+let load_modtype i ((sp,kn),sobjs) = do_modtype i sp (mp_of_kn kn) sobjs
+let subst_modtype (subst,sobjs) = subst_sobjs subst sobjs
+let classify_modtype sobjs = Substitute sobjs
 
-  (* We enrich the global environment *)
-  let _ =
-    match entry with
-      | None ->
-	  anomaly "You must not recache interactive module types!"
-      | Some (mte,inl) ->
-	  if mp <> Global.add_modtype (basename sp) mte inl then
-	    anomaly "Kernel and Library names do not match"
+let open_modtype i ((sp,kn),_) =
+  let mp = mp_of_kn kn in
+  let mp' =
+    try Nametab.locate_modtype (qualid_of_path sp)
+    with Not_found ->
+      anomaly (pr_path sp ++ str " should already exist!");
   in
+  assert (ModPath.equal mp mp');
+  Nametab.push_modtype (Nametab.Exactly i) sp mp
 
-  (* Using declare_modtype should lead here, where we check
-     that any given subtyping is indeed accurate *)
-  check_subtypes_mt mp sub_mty_l;
+let (in_modtype : substitutive_objects -> obj),
+    (out_modtype : obj -> substitutive_objects) =
+  declare_object_full {(default_object "MODULE TYPE") with
+      cache_function = cache_modtype;
+      open_function = open_modtype;
+      load_function = load_modtype;
+      subst_function = subst_modtype;
+      classify_function = classify_modtype }
 
-  if Nametab.exists_modtype sp then
-    errorlabstrm "cache_modtype"
-      (pr_path sp ++ str " already exists") ;
 
-  Nametab.push_modtype (Nametab.Until 1) sp mp;
+(** {6 Declaration of substitutive objects for Include} *)
 
-  modtypetab := MPmap.add mp modtypeobjs !modtypetab
+let do_include do_load do_open i ((sp,kn),aobjs) =
+  let dir = Libnames.dirpath sp in
+  let mp = KerName.modpath kn in
+  let prefix = (dir,(mp,DirPath.empty)) in
+  let o = expand_aobjs aobjs in
+  if do_load then Lib.load_objects i prefix o;
+  if do_open then Lib.open_objects i prefix o
 
+let cache_include = do_include true true 1
+let load_include = do_include true false
+let open_include = do_include false true
+let subst_include (subst,aobjs) = subst_aobjs subst aobjs
+let classify_include aobjs = Substitute aobjs
 
-let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
-  assert (entry = None);
+let (in_include : algebraic_objects -> obj),
+    (out_include : obj -> algebraic_objects) =
+  declare_object_full {(default_object "INCLUDE") with
+    cache_function = cache_include;
+    load_function = load_include;
+    open_function = open_include;
+    subst_function = subst_include;
+    classify_function = classify_include }
 
-  if Nametab.exists_modtype sp then
-    errorlabstrm "cache_modtype"
-      (pr_path sp ++ str " already exists") ;
 
-  Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn);
+(** {6 Handler for missing entries in ModSubstObjs} *)
 
-  modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
+(** Since the inner of Module Types are not added by default to
+    the ModSubstObjs table, we compensate this by explicit traversal
+    of Module Types inner objects when needed. Quite a hack... *)
 
+let mp_id mp id = MPdot (mp, Label.of_id id)
 
-let open_modtype i ((sp,kn),(entry,_,_)) =
-  assert (entry = None);
+let rec register_mod_objs mp (id,obj) = match object_tag obj with
+  | "MODULE" -> ModSubstObjs.set (mp_id mp id) (out_module obj)
+  | "MODULE TYPE" -> ModSubstObjs.set (mp_id mp id) (out_modtype obj)
+  | "INCLUDE" ->
+    List.iter (register_mod_objs mp) (expand_aobjs (out_include obj))
+  | _ -> ()
 
-  if
-    try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn)
-    with Not_found -> true
-  then
-    errorlabstrm ("open_modtype")
-      (pr_path sp ++ str " should already exist!");
+let handle_missing_substobjs mp = match mp with
+  | MPdot (mp',l) ->
+    let objs = expand_sobjs (ModSubstObjs.get mp') in
+    List.iter (register_mod_objs mp') objs;
+    ModSubstObjs.get mp
+  | _ ->
+    assert false (* Only inner parts of module types should be missing *)
 
-  Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
+let () = ModSubstObjs.set_missing_handler handle_missing_substobjs
 
-let subst_modtype (subst,(entry,(mbids,mp,objs),_)) =
-  assert (entry = None);
-  (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[])
 
-let classify_modtype (_,substobjs,_) =
-  Substitute (None,substobjs,[])
 
-type modtype_obj =
-    (module_struct_entry * Entries.inline) option (* will be None in vo *)
-    * substitutive_objects
-    * module_type_body list
+(** {6 From module expression to substitutive objects} *)
 
-let in_modtype : modtype_obj -> obj =
-    declare_object {(default_object "MODULE TYPE") with
-      cache_function = cache_modtype;
-      open_function = open_modtype;
-      load_function = load_modtype;
-      subst_function = subst_modtype;
-      classify_function = classify_modtype }
+(** Turn a chain of [MSEapply] into the head module_path and the
+    list of module_path parameters (deepest param coming first).
+    The left part of a [MSEapply] must be either [MSEident] or
+    another [MSEapply]. *)
 
-let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
-  if mbids<>[] then anomaly "Unexpected functor objects";
-  let rec replace_idl = function
-    | _,[] -> []
-    | id::idl,(id',obj)::tail when id = id' ->
-      if object_tag obj <> "MODULE" then anomaly "MODULE expected!";
-      let substobjs =
-	if idl = [] then
-	  let mp' = MPdot(mp, label_of_id id) in
-	  mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs
-	else
-	  replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp
-      in
-      (id, in_module substobjs)::tail
-    | idl,lobj::tail -> lobj::replace_idl (idl,tail)
-  in
-  (mbids, mp, replace_idl (idl,lib_stack))
-
-let discr_resolver mb = match mb.mod_type with
-  | SEBstruct _ -> Some mb.mod_delta
-  | _ -> None (* when mp is a functor *)
-
-(* Small function to avoid module typing during substobjs retrivial  *)
-let rec get_objs_modtype_application env = function
-| MSEident mp -> 
-    MPmap.find mp !modtypetab,Environ.lookup_modtype mp env,[]
-| MSEapply (fexpr, MSEident mp) -> 
-    let objs,mtb,mp_l= get_objs_modtype_application env fexpr in
-      objs,mtb,mp::mp_l
-| MSEapply (_,mexpr) ->
-    Modops.error_application_to_not_path mexpr
-| _ -> error "Application of a non-functor."
+let get_applications mexpr =
+  let rec get params = function
+    | MEident mp -> mp, params
+    | MEapply (fexpr, mp) -> get (mp::params) fexpr
+    | MEwith _ -> error "Non-atomic functor application."
+  in get [] mexpr
+
+(** Create the substitution corresponding to some functor applications *)
 
 let rec compute_subst env mbids sign mp_l inl =
   match mbids,mp_l with
     | _,[] -> mbids,empty_subst
     | [],r -> error "Application of a functor with too few arguments."
     | mbid::mbids,mp::mp_l ->
-	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
 	let mb = Environ.lookup_module mp env in
 	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
-	let resolver = match discr_resolver mb with
-	  | None -> empty_delta_resolver
-	  | Some mp_delta ->
-	      Modops.inline_delta_resolver env inl mp farg_id farg_b mp_delta
+	let resolver =
+          if Modops.is_functor mb.mod_type then empty_delta_resolver
+          else
+            Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta
 	in
 	mbid_left,join (map_mbid mbid mp resolver) subst
 
-let rec get_modtype_substobjs env mp_from inline = function
-    MSEident ln -> 
-      MPmap.find ln !modtypetab 
-  | MSEfunctor (mbid,_,mte) ->
-      let (mbids, mp, objs) = get_modtype_substobjs env mp_from inline mte in
-	(mbid::mbids, mp, objs)
-  | MSEwith (mty, With_Definition _) ->
-      get_modtype_substobjs env mp_from inline mty
-  | MSEwith (mty, With_Module (idl,mp1)) -> 
-      let substobjs = get_modtype_substobjs env mp_from inline mty in
-      let modobjs = MPmap.find mp1 !modtab_substobjs in
-	replace_module_object idl substobjs modobjs mp1
-  | MSEapply (fexpr, MSEident mp) as me ->
-      let (mbids, mp1, objs),mtb_mp1,mp_l =
-	get_objs_modtype_application env me in
-      let mbids_left,subst =
-	compute_subst env mbids mtb_mp1.typ_expr (List.rev mp_l) inline
-      in
-      (mbids_left, mp1,subst_objects subst objs)
-  | MSEapply (_,mexpr) ->
-      Modops.error_application_to_not_path mexpr
-
-(* push names of bound modules (and their components) to Nametab *)
-(* add objects associated to them *)
-let process_module_bindings argids args =
-  let process_arg id (mbid,(mty,ann)) =
-    let dir = make_dirpath [id] in
-    let mp = MPbound mbid in
-    let (mbids,mp_from,objs) =
-      get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in
-    let substobjs = (mbids,mp,subst_objects
-		       (map_mp mp_from mp empty_delta_resolver) objs)in
-      do_module false "start" load_objects 1 dir mp substobjs []
+(** Create the objects of a "with Module" structure. *)
+
+let rec replace_module_object idl mp0 objs0 mp1 objs1 =
+  match idl, objs0 with
+  | _,[] -> []
+  | id::idl,(id',obj)::tail when Id.equal id id' ->
+    assert (object_has_tag obj "MODULE");
+    let mp_id = MPdot(mp0, Label.of_id id) in
+    let objs = match idl with
+      | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1
+      | _ ->
+        let objs_id = expand_sobjs (out_module obj) in
+        replace_module_object idl mp_id objs_id mp1 objs1
     in
-      List.iter2 process_arg argids args
-
-(* Same with module_type_body *)
-
-let rec seb2mse = function
-  | SEBident mp -> MSEident mp
-  | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s')
-  | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp))
-  | SEBwith (s,With_definition_body(l,cb)) ->
-      (match cb.const_body with
-	| Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c))
-	| _ -> assert false)
-  | _ -> failwith "seb2mse: received a non-atomic seb"
-
-let process_module_seb_binding mbid seb =
-  process_module_bindings [id_of_mbid mbid]
-    [mbid,
-     (seb2mse seb,
-      { ann_inline = DefaultInline; ann_scope_subst = [] })]
-
-let intern_args interp_modtype (idl,(arg,ann)) =
-  let inl = inline_annot ann in
+    (id, in_module ([], Objs objs))::tail
+  | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1
+
+let type_of_mod mp env = function
+  |true -> (Environ.lookup_module mp env).mod_type
+  |false -> (Environ.lookup_modtype mp env).mod_type
+
+let rec get_module_path = function
+  |MEident mp -> mp
+  |MEwith (me,_) -> get_module_path me
+  |MEapply (me,_) -> get_module_path me
+
+(** Substitutive objects of a module expression (or module type) *)
+
+let rec get_module_sobjs is_mod env inl = function
+  |MEident mp ->
+    begin match ModSubstObjs.get mp with
+    |(mbids,Objs _) when not (ModPath.is_bound mp) ->
+      (mbids,Ref (mp, empty_subst)) (* we create an alias *)
+    |sobjs -> sobjs
+    end
+  |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty
+  |MEwith (mty, WithMod (idl,mp1)) ->
+    assert (not is_mod);
+    let sobjs0 = get_module_sobjs is_mod env inl mty in
+    assert (sobjs_no_functor sobjs0);
+    (* For now, we expanse everything, to be safe *)
+    let mp0 = get_module_path mty in
+    let objs0 = expand_sobjs sobjs0 in
+    let objs1 = expand_sobjs (ModSubstObjs.get mp1) in
+    ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1))
+  |MEapply _ as me ->
+    let mp1, mp_l = get_applications me in
+    let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in
+    let typ = type_of_mod mp1 env is_mod in
+    let mbids_left,subst = compute_subst env mbids typ mp_l inl in
+    (mbids_left, subst_aobjs subst aobjs)
+
+let get_functor_sobjs is_mod env inl (params,mexpr) =
+  let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in
+  (List.map fst params @ mbids, aobjs)
+
+
+(** {6 Handling of module parameters} *)
+
+(** For printing modules, [process_module_binding] adds names of
+    bound module (and its components) to Nametab. It also loads
+    objects associated to it. *)
+
+let process_module_binding mbid me =
+  let dir = DirPath.make [MBId.to_id mbid] in
+  let mp = MPbound mbid in
+  let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in
+  let subst = map_mp (get_module_path me) mp empty_delta_resolver in
+  let sobjs = subst_sobjs subst sobjs in
+  do_module false Lib.load_objects 1 dir mp sobjs []
+
+(** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ)
+    i.e. possibly multiple names with the same module type.
+    Global environment is updated on the fly.
+    Objects in these parameters are also loaded.
+    Output is accumulated on top of [acc] (in reverse order). *)
+
+let intern_arg interp_modast acc (idl,(typ,ann)) =
+  let inl = inl2intopt ann in
   let lib_dir = Lib.library_dp() in
-  let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in
-  let mty = interp_modtype (Global.env()) arg in
-  let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
-  let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
-    (MPbound (List.hd mbids)) inl mty in
-  List.map2
-    (fun dir mbid ->
-       let resolver = Global.add_module_parameter mbid mty inl in
-       let mp = MPbound mbid in
-       let substobjs = (mbi,mp,subst_objects
-			  (map_mp mp_from mp resolver) objs) in
-	 do_module false "interp" load_objects 1 dir mp substobjs [];
-	 (mbid,(mty,inl)))
-    dirs mbids
-
-let start_module_ interp_modtype export id args res fs =
-  let mp = Global.start_module id in
-  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-  let res_entry_o, sub_body_l = match res with
-    | Enforce (res,ann) ->
-        let inl = inline_annot ann in
-	let mte = interp_modtype (Global.env()) res in
-	let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in
-	Some (mte,inl), []
-    | Check resl ->
-	None, build_subtypes interp_modtype mp arg_entries resl
-  in
-  let mbids = List.map fst arg_entries in
-  openmod_info:=(mp,mbids,res_entry_o,sub_body_l);
-  let prefix = Lib.start_module export id mp fs in
-  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-  Lib.add_frozen_state (); mp
+  let env = Global.env() in
+  let mty,_ = interp_modast env ModType typ in
+  let sobjs = get_module_sobjs false env inl mty in
+  let mp0 = get_module_path mty in
+  List.fold_left
+    (fun acc (_,id) ->
+      let dir = DirPath.make [id] in
+      let mbid = MBId.make lib_dir id in
+      let mp = MPbound mbid in
+      let resolver = Global.add_module_parameter mbid mty inl in
+      let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
+      do_module false Lib.load_objects 1 dir mp sobjs [];
+      (mbid,mty,inl)::acc)
+    acc idl
+
+(** Process a list of declarations of functor parameters
+    (Id11 .. Id1n : Typ1)..(Idk1 .. Idkm : Typk)
+    Global environment is updated on the fly.
+    The calls to [interp_modast] should be interleaved with these
+    env updates, otherwise some "with Definition" could be rejected.
+    Returns a list of mbids and entries (in reversed order).
+
+    This used to be a [List.concat (List.map ...)], but this should
+    be more efficient and independent of [List.map] eval order.
+*)
 
+let intern_args interp_modast params =
+  List.fold_left (intern_arg interp_modast) [] params
 
-let end_module () =
 
-  let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
-  let mp,mbids, res_o, sub_l = !openmod_info in
-  let substitute, keep, special = Lib.classify_segment lib_stack in
-
-  let mp_from,substobjs, keep, special = try
-    match res_o with
-      | None ->
-	  (* the module is not sealed *)
-	  None,( mbids, mp, substitute), keep, special
-      | Some (MSEident ln as mty, inline) ->
-	  let (mbids1,mp1,objs) =
-	    get_modtype_substobjs (Global.env()) mp inline mty in
-	  Some mp1,(mbids@mbids1,mp1,objs), [], []
-      | Some (MSEwith _ as mty, inline) ->
-	  let (mbids1,mp1,objs) =
-	    get_modtype_substobjs (Global.env()) mp inline mty in
-	  Some mp1,(mbids@mbids1,mp1,objs), [], []
-      | Some (MSEfunctor _, _) ->
-	  anomaly "Funsig cannot be here..."
-      | Some (MSEapply _ as mty, inline) ->
-	  let (mbids1,mp1,objs) =
-	    get_modtype_substobjs (Global.env()) mp inline mty in
-	  Some mp1,(mbids@mbids1,mp1,objs), [], []
-  with
-	Not_found -> anomaly "Module objects not found..."
-  in
-    (* must be called after get_modtype_substobjs, because of possible
-     dependencies on functor arguments *)
+(** {6 Auxiliary functions concerning subtyping checks} *)
 
-  let id = basename (fst oldoname) in
-  let mp,resolver = Global.end_module fs id res_o in
+let check_sub mtb sub_mtb_l =
+  (* The constraints are checked and forgot immediately : *)
+  ignore (List.fold_right
+	    (fun sub_mtb env ->
+	       Environ.add_constraints
+		 (Subtyping.check_subtypes env mtb sub_mtb) env)
+	    sub_mtb_l (Global.env()))
 
-  check_subtypes mp sub_l;
+(** This function checks if the type calculated for the module [mp] is
+    a subtype of all signatures in [sub_mtb_l]. Uses only the global
+    environment. *)
 
-(* we substitute objects if the module is 
-   sealed by a signature (ie. mp_from != None *)
-  let substobjs = match mp_from,substobjs with
-      None,_ -> substobjs
-    | Some mp_from,(mbids,_,objs) ->
-	(mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) 
+let check_subtypes mp sub_mtb_l =
+  let mb =
+    try Global.lookup_module mp with Not_found -> assert false
   in
-  let node = in_module substobjs in
-  let objects =
-    if keep = [] || mbids <> [] then
-      special@[node]   (* no keep objects or we are defining a functor *)
-    else
-      special@[node;in_modkeep keep]   (* otherwise *)
+  let mtb = Modops.module_type_of_module mb in
+  check_sub mtb sub_mtb_l
+
+(** Same for module type [mp] *)
+
+let check_subtypes_mt mp sub_mtb_l =
+  let mtb =
+    try Global.lookup_modtype mp with Not_found -> assert false
   in
-  let newoname = Lib.add_leaves id objects in
+  check_sub mtb sub_mtb_l
 
-    if (fst newoname) <> (fst oldoname) then
-      anomaly "Names generated on start_ and end_module do not match";
-    if mp_of_kn (snd newoname) <> mp then
-      anomaly "Kernel and Library names do not match";
+(** Create a params entry.
+    In [args], the youngest module param now comes first. *)
 
-    Lib.add_frozen_state () (* to prevent recaching *);
-    mp
+let mk_params_entry args =
+  List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args
 
+(** Create a functor type struct.
+    In [args], the youngest module param now comes first. *)
 
+let mk_funct_type env args seb0 =
+  List.fold_left
+    (fun seb (arg_id,arg_t,arg_inl) ->
+      let mp = MPbound arg_id in
+      let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in
+      MoreFunctor(arg_id,arg_t,seb))
+    seb0 args
 
-let module_objects mp =
-  let prefix,objects = MPmap.find mp !modtab_objects in
-    segment_of_objects prefix objects
+(** Prepare the module type list for check of subtypes *)
 
+let build_subtypes interp_modast env mp args mtys =
+  List.map
+    (fun (m,ann) ->
+       let inl = inl2intopt ann in
+       let mte,_ = interp_modast env ModType m in
+       let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in
+       { mtb with mod_type = mk_funct_type env args mtb.mod_type })
+    mtys
 
 
-(************************************************************************)
-(* libraries *)
+(** {6 Current module information}
 
-type library_name = dir_path
+    This information is stored by each [start_module] for use
+    in a later [end_module]. *)
 
-(* The first two will form substitutive_objects, the last one is keep *)
-type library_objects =
-    module_path * lib_objects * lib_objects
+type current_module_info = {
+  cur_typ : (module_struct_entry * int option) option; (** type via ":" *)
+  cur_typs : module_type_body list (** types via "<:" *)
+}
 
+let default_module_info = { cur_typ = None; cur_typs = [] }
 
-let register_library dir cenv objs digest =
-  let mp = MPfile dir in
-  let substobjs, keep =
-  try 
-    ignore(Global.lookup_module mp);
-    (* if it's in the environment, the cached objects should be correct *)
-    Dirmap.find dir !library_cache
-  with Not_found ->
-    if mp <> Global.import cenv digest then
-      anomaly "Unexpected disk module name";
-    let mp,substitute,keep = objs in
-    let substobjs = [], mp, substitute in
-    let modobjs = substobjs, keep in
-    library_cache := Dirmap.add dir modobjs !library_cache;
-      modobjs
-  in
-    do_module false "register_library" load_objects 1 dir mp substobjs keep
+let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO"
 
-let start_library dir =
-  let mp = Global.start_library dir in
-  openmod_info:=mp,[],None,[];
-  Lib.start_compilation dir mp;
-  Lib.add_frozen_state ()
 
-let end_library_hook = ref ignore
-let set_end_library_hook f = end_library_hook := f
+(** {6 Current module type information}
 
-let end_library dir =
-  !end_library_hook();
-  let prefix, lib_stack = Lib.end_compilation dir in
-  let mp,cenv = Global.export dir in
-  let substitute, keep, _ = Lib.classify_segment lib_stack in
-    cenv,(mp,substitute,keep)
+   This information is stored by each [start_modtype] for use
+   in a later [end_modtype]. *)
 
+let openmodtype_info =
+  Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO"
 
-(* implementation of Export M and Import M *)
 
+(** {6 Modules : start, end, declare} *)
 
-let really_import_module mp =
-  let prefix,objects = MPmap.find mp !modtab_objects in
-    open_objects 1 prefix objects
+module RawModOps = struct
 
+let start_module interp_modast export id args res fs =
+  let mp = Global.start_module id in
+  let arg_entries_r = intern_args interp_modast args in
+  let env = Global.env () in
+  let res_entry_o, subtyps = match res with
+    | Enforce (res,ann) ->
+        let inl = inl2intopt ann in
+	let mte,_ = interp_modast env ModType res in
+        (* We check immediately that mte is well-formed *)
+	let _ = Mod_typing.translate_mse env None inl mte in
+	Some (mte,inl), []
+    | Check resl ->
+	None, build_subtypes interp_modast env mp arg_entries_r resl
+  in
+  openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
+  let prefix = Lib.start_module export id mp fs in
+  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
+  Lib.add_frozen_state (); mp
 
-let cache_import (_,(_,mp)) =
-(* for non-substitutive exports:
-  let mp = Nametab.locate_module (qualid_of_dirpath dir) in  *)
-  really_import_module mp
+let end_module () =
+  let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
+  let substitute, keep, special = Lib.classify_segment lib_stack in
+  let m_info = !openmod_info in
 
-let classify_import (export,_ as obj) =
-  if export then Substitute obj else Dispose
+  (* For sealed modules, we use the substitutive objects of their signatures *)
+  let sobjs0, keep, special = match m_info.cur_typ with
+    | None -> ([], Objs substitute), keep, special
+    | Some (mty, inline) ->
+      get_module_sobjs false (Global.env()) inline mty, [], []
+  in
+  let id = basename (fst oldoname) in
+  let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in
+  let sobjs = let (ms,objs) = sobjs0 in (mbids@ms,objs) in
 
-let subst_import (subst,(export,mp as obj)) =
-   let mp' = subst_mp subst mp in
-    if mp'==mp then obj else
-      (export,mp')
+  check_subtypes mp m_info.cur_typs;
 
-let in_import =
-  declare_object {(default_object "IMPORT MODULE") with
-		    cache_function = cache_import;
-		    open_function = (fun i o -> if i=1 then cache_import o);
-		    subst_function = subst_import;
-		    classify_function = classify_import }
+  (* We substitute objects if the module is sealed by a signature *)
+  let sobjs =
+    match m_info.cur_typ with
+      | None -> sobjs
+      | Some (mty, _) ->
+        subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs
+  in
+  let node = in_module sobjs in
+  (* We add the keep objects, if any, and if this isn't a functor *)
+  let objects = match keep, mbids with
+    | [], _ | _, _ :: _ -> special@[node]
+    | _ -> special@[node;in_modkeep keep]
+  in
+  let newoname = Lib.add_leaves id objects in
 
+  (* Name consistency check : start_ vs. end_module, kernel vs. library *)
+  assert (eq_full_path (fst newoname) (fst oldoname));
+  assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
 
-let import_module export mp =
-  Lib.add_anonymous_leaf (in_import (export,mp))
+  Lib.add_frozen_state () (* to prevent recaching *);
+  mp
 
-(************************************************************************)
-(* module types *)
+let declare_module interp_modast id args res mexpr_o fs =
+  (* We simulate the beginning of an interactive module,
+     then we adds the module parameters to the global env. *)
+  let mp = Global.start_module id in
+  let arg_entries_r = intern_args interp_modast args in
+  let params = mk_params_entry arg_entries_r in
+  let env = Global.env () in
+  let mty_entry_o, subs, inl_res = match res with
+    | Enforce (mty,ann) ->
+        Some (fst (interp_modast env ModType mty)), [], inl2intopt ann
+    | Check mtys ->
+	None, build_subtypes interp_modast env mp arg_entries_r mtys,
+        default_inline ()
+  in
+  let mexpr_entry_o, inl_expr = match mexpr_o with
+    | None -> None, default_inline ()
+    | Some (mexpr,ann) ->
+      Some (fst (interp_modast env Module mexpr)), inl2intopt ann
+  in
+  let entry = match mexpr_entry_o, mty_entry_o with
+    | None, None -> assert false (* No body, no type ... *)
+    | None, Some typ -> MType (params, typ)
+    | Some body, otyp -> MExpr (params, body, otyp)
+  in
+  let sobjs, mp0 = match entry with
+    | MType (_,mte) | MExpr (_,_,Some mte) ->
+      get_functor_sobjs false env inl_res (params,mte), get_module_path mte
+    | MExpr (_,me,None) ->
+      get_functor_sobjs true env inl_expr (params,me), get_module_path me
+  in
+  (* Undo the simulated interactive building of the module
+     and declare the module as a whole *)
+  Summary.unfreeze_summaries fs;
+  let inl = match inl_expr with
+  | None -> None
+  | _ -> inl_res
+  in
+  let mp_env,resolver = Global.add_module id entry inl in
+
+  (* Name consistency check : kernel vs. library *)
+  assert (ModPath.equal mp (mp_of_kn (Lib.make_kn id)));
+  assert (ModPath.equal mp mp_env);
+
+  check_subtypes mp subs;
 
-let start_modtype_ interp_modtype id args mtys fs =
+  let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
+  ignore (Lib.add_leaf id (in_module sobjs));
+  mp
+
+end
+
+(** {6 Module types : start, end, declare} *)
+
+module RawModTypeOps = struct
+
+let start_modtype interp_modast id args mtys fs =
   let mp = Global.start_modtype id in
-  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-  let sub_mty_l = build_subtypes interp_modtype mp arg_entries mtys in
-  let mbids = List.map fst arg_entries in
-  openmodtype_info := mbids, sub_mty_l;
+  let arg_entries_r = intern_args interp_modast args in
+  let env = Global.env () in
+  let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
+  openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
   Lib.add_frozen_state (); mp
 
-
 let end_modtype () =
   let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in
   let id = basename (fst oldoname) in
   let substitute, _, special = Lib.classify_segment lib_stack in
-  let mbids, sub_mty_l = !openmodtype_info in
-  let mp = Global.end_modtype fs id in
-  let modtypeobjs = mbids, mp, substitute in
+  let sub_mty_l = !openmodtype_info in
+  let mp, mbids = Global.end_modtype fs id in
+  let modtypeobjs = (mbids, Objs substitute) in
   check_subtypes_mt mp sub_mty_l;
-  let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs,[])])
+  let oname = Lib.add_leaves id (special@[in_modtype modtypeobjs])
   in
-  if fst oname <> fst oldoname then
-    anomaly
-      "Section paths generated on start_ and end_modtype do not match";
-  if (mp_of_kn (snd oname)) <> mp then
-    anomaly
-      "Kernel and Library names do not match";
+  (* Check name consistence : start_ vs. end_modtype, kernel vs. library *)
+  assert (eq_full_path (fst oname) (fst oldoname));
+  assert (ModPath.equal (mp_of_kn (snd oname)) mp);
 
   Lib.add_frozen_state ()(* to prevent recaching *);
   mp
 
-
-let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
-  let inl = inline_annot ann in
-  let mmp = Global.start_modtype id in
-  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-  let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
-  (* NB: check of subtyping will be done in cache_modtype *)
-  let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in
-  let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp inl entry in
-  (* Undo the simulated interactive building of the module type *)
-  (* and declare the module type as a whole *)
-
-  register_scope_subst ann.ann_scope_subst;
-  let substobjs = (mbids,mmp,
-		   subst_objects (map_mp mp_from mmp empty_delta_resolver) objs)
-  in
-  reset_scope_subst ();
+let declare_modtype interp_modast id args mtys (mty,ann) fs =
+  let inl = inl2intopt ann in
+  (* We simulate the beginning of an interactive module,
+     then we adds the module parameters to the global env. *)
+  let mp = Global.start_modtype id in
+  let arg_entries_r = intern_args interp_modast args in
+  let params = mk_params_entry arg_entries_r in
+  let env = Global.env () in
+  let entry = params, fst (interp_modast env ModType mty) in
+  let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
+  let sobjs = get_functor_sobjs false env inl entry in
+  let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
+  let sobjs = subst_sobjs subst sobjs in
+
+  (* Undo the simulated interactive building of the module type
+     and declare the module type as a whole *)
   Summary.unfreeze_summaries fs;
-  ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
-  mmp
-
-
-(* Small function to avoid module typing during substobjs retrivial  *)
-let rec get_objs_module_application env = function
-| MSEident mp -> 
-    MPmap.find mp !modtab_substobjs,Environ.lookup_module mp env,[]
-| MSEapply (fexpr, MSEident mp) -> 
-    let objs,mtb,mp_l= get_objs_module_application env fexpr in
-      objs,mtb,mp::mp_l
-| MSEapply (_,mexpr) ->
-    Modops.error_application_to_not_path mexpr
-| _ -> error "Application of a non-functor."
-
-
-let rec get_module_substobjs env mp_from inl = function
-  | MSEident mp -> MPmap.find mp !modtab_substobjs
-  | MSEfunctor (mbid,mty,mexpr) ->
-       let (mbids, mp, objs) = get_module_substobjs env mp_from inl mexpr in
-	(mbid::mbids, mp, objs)
-  | MSEapply (fexpr, MSEident mp) as me ->
-      let (mbids, mp1, objs),mb_mp1,mp_l =
-	get_objs_module_application env me
-      in
-      let mbids_left,subst =
-	compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) inl in
-      (mbids_left, mp1,subst_objects subst objs)
-  | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr
-  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty
-  | MSEwith (mty, With_Module (idl,mp)) -> assert false
-
-
-let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
-  let mmp = Global.start_module id in
-  let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
-  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
-  let env = Global.env() in
-  let mty_entry_o, subs, inl_res = match res with
-    | Enforce (mty,ann) ->
-        Some (funct interp_modtype mty), [], inline_annot ann
-    | Check mtys ->
-	None, build_subtypes interp_modtype mmp arg_entries mtys,
-        default_inline ()
-  in
- 
-  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
-  let mexpr_entry_o, inl_expr, scl = match mexpr_o with
-    | None -> None, default_inline (), []
-    | Some (mexpr,ann) ->
-      Some (funct interp_modexpr mexpr), inline_annot ann, ann.ann_scope_subst
 
-  in
-  let entry =
-    {mod_entry_type = mty_entry_o;
-     mod_entry_expr = mexpr_entry_o }
-  in
+  (* We enrich the global environment *)
+  let mp_env = Global.add_modtype id entry inl in
 
-  let substobjs =
-    match entry with
-      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
-      | _ -> anomaly "declare_module: No type, no body ..."
-  in
-  let (mbids,mp_from,objs) = substobjs in
-  (* Undo the simulated interactive building of the module *)
-  (* and declare the module as a whole *)
-  Summary.unfreeze_summaries fs;
-  let mp = mp_of_kn (Lib.make_kn id) in
-  let inl = if inl_expr = None then None else inl_res in (*PLTODO *)
-  let mp_env,resolver = Global.add_module id entry inl in
+  (* Name consistency check : kernel vs. library *)
+  assert (ModPath.equal mp_env mp);
 
-  if mp_env <> mp then anomaly "Kernel and Library names do not match";
+  (* Subtyping checks *)
+  check_subtypes_mt mp sub_mty_l;
 
-  
-  check_subtypes mp subs;
-  register_scope_subst scl;
-  let substobjs = (mbids,mp_env,
-		   subst_objects(map_mp mp_from mp_env resolver) objs) in
-  reset_scope_subst ();
-  ignore (add_leaf
-	    id
-	    (in_module substobjs));
-  mmp
-
-(* Include *)
-
-let rec subst_inc_expr subst me =
-  match me with
-    | MSEident mp -> MSEident (subst_mp subst mp)
-    | MSEwith (me,With_Module(idl,mp)) ->
-	MSEwith (subst_inc_expr subst me,
-		 With_Module(idl,subst_mp subst mp))
-    | MSEwith (me,With_Definition(idl,const))->
-	let const1 = Mod_subst.from_val const in
-	let force = Mod_subst.force subst_mps in
-	MSEwith (subst_inc_expr subst me,
-		 With_Definition(idl,force (subst_substituted
-					   subst const1)))
-    | MSEapply (me1,me2) ->
-	MSEapply (subst_inc_expr subst me1,
-		  subst_inc_expr subst me2)
-    | MSEfunctor(mbid,me1,me2) ->
-        MSEfunctor (mbid, subst_inc_expr subst me1, subst_inc_expr subst me2)
-
-let lift_oname (sp,kn) =
-  let mp,_,_ = Names.repr_kn kn in
-  let dir,_ = Libnames.repr_path sp in
-    (dir,mp)
-
-let cache_include (oname,(me,(mbis,mp1,objs))) =
-  let dir,mp1 = lift_oname oname in
-  let prefix = (dir,(mp1,empty_dirpath)) in
-    load_objects 1 prefix objs;
-    open_objects 1 prefix objs
-
-let load_include  i (oname,(me,(mbis,mp1,objs))) =
-  let dir,mp1 = lift_oname oname in
-  let prefix = (dir,(mp1,empty_dirpath)) in
-    load_objects i prefix objs
-
-let open_include i (oname,(me,(mbis,mp1,objs))) =
-  let dir,mp1 = lift_oname oname in
-  let prefix = (dir,(mp1,empty_dirpath)) in
-    open_objects i prefix objs
-
-let subst_include (subst,(me,substobj)) =
-  let (mbids,mp,objs) = substobj in
-  let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in
-    (subst_inc_expr subst me,substobjs)
-
-let classify_include (me,substobjs) = Substitute (me,substobjs)
-
-type include_obj = module_struct_entry * substitutive_objects
-
-let (in_include : include_obj -> obj),
-    (out_include : obj -> include_obj) =
-  declare_object_full {(default_object "INCLUDE") with
-    cache_function = cache_include;
-    load_function = load_include;
-    open_function = open_include;
-    subst_function = subst_include;
-    classify_function = classify_include }
+  ignore (Lib.add_leaf id (in_modtype sobjs));
+  mp
 
-let rec include_subst env mb mbids sign inline =
-  match mbids with
-    | [] -> empty_subst
-    | mbid::mbids ->
-	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
-	let subst = include_subst env mb mbids fbody_b inline in
-	let mp_delta =
-	  Modops.inline_delta_resolver env inline mb.mod_mp
-	    farg_id farg_b mb.mod_delta
-	in
-	join (map_mbid mbid mb.mod_mp mp_delta) subst
-
-exception NothingToDo
-
-let get_includeself_substobjs env objs me is_mod inline =
-  try
-    let mb_mp = match me with
-      | MSEident mp ->
-	  if is_mod then
-	    Environ.lookup_module mp env
-	  else
-	    Modops.module_body_of_type mp (Environ.lookup_modtype mp env)
-      | MSEapply(fexpr, MSEident p) as mexpr ->
-	  let _,mb_mp,mp_l =
-	    if is_mod then
-	      get_objs_module_application env mexpr
-	    else
-	      let o,mtb_mp,mp_l = get_objs_modtype_application env mexpr in
-	      o,Modops.module_body_of_type mtb_mp.typ_mp mtb_mp,mp_l
-	  in
-	  List.fold_left
-	    (fun mb _ ->
-	       match mb.mod_type with
-		 |  SEBfunctor(_,_,str) -> {mb with mod_type = str}
-		 | _ -> error "Application of a functor with too much arguments.")
-	    mb_mp mp_l
-      | _ -> raise NothingToDo
+end
+
+(** {6 Include} *)
+
+module RawIncludeOps = struct
+
+let rec include_subst env mp reso mbids sign inline = match mbids with
+  | [] -> empty_subst
+  | mbid::mbids ->
+    let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
+    let subst = include_subst env mp reso mbids fbody_b inline in
+    let mp_delta =
+      Modops.inline_delta_resolver env inline mp farg_id farg_b reso
     in
-    let (mbids,mp_self,objects) = objs in
-    let mb = Global.pack_module() in
-    let subst = include_subst env mb mbids mb_mp.mod_type inline in
-    ([],mp_self,subst_objects subst objects)
-  with NothingToDo -> objs
+    join (map_mbid mbid mp mp_delta) subst
 
+let rec decompose_functor mpl typ =
+  match mpl, typ with
+  | [], _ -> typ
+  | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
+  | _ -> error "Application of a functor with too much arguments."
 
+exception NoIncludeSelf
 
+let type_of_incl env is_mod = function
+  |MEident mp -> type_of_mod mp env is_mod
+  |MEapply _ as me ->
+    let mp0, mp_l = get_applications me in
+    decompose_functor mp_l (type_of_mod mp0 env is_mod)
+  |MEwith _ -> raise NoIncludeSelf
 
-let declare_one_include_inner annot (me,is_mod) =
+let declare_one_include interp_modast (me_ast,annot) =
   let env = Global.env() in
-  let mp1,_ = current_prefix () in
-  let inl = inline_annot annot in
-  let (mbids,mp,objs)=
-    if is_mod then
-      get_module_substobjs env mp1 inl me
-    else
-      get_modtype_substobjs env mp1 inl me in
-  let (mbids,mp,objs) =
-    if mbids <> [] then
-      get_includeself_substobjs env (mbids,mp,objs) me is_mod inl
-    else
-      (mbids,mp,objs) in
-  let id = current_mod_id() in
-  let resolver =  Global.add_include me is_mod inl in
-  register_scope_subst annot.ann_scope_subst;
-  let substobjs = (mbids,mp1,
-		   subst_objects (map_mp mp mp1 resolver) objs) in
-  reset_scope_subst ();
-  ignore (add_leaf id (in_include (me, substobjs)))
-
-let declare_one_include interp_struct (me_ast,annot) =
-  declare_one_include_inner annot
-    (interp_struct (Global.env()) me_ast)
-
-let declare_include_ interp_struct me_asts =
-  List.iter (declare_one_include interp_struct) me_asts
-
-(** Versions of earlier functions taking care of the freeze/unfreeze
-    of summaries *)
+  let me,kind = interp_modast env ModAny me_ast in
+  let is_mod = (kind == Module) in
+  let cur_mp = Lib.current_mp () in
+  let inl = inl2intopt annot in
+  let mbids,aobjs = get_module_sobjs is_mod env inl me in
+  let subst_self =
+    try
+      if List.is_empty mbids then raise NoIncludeSelf;
+      let typ = type_of_incl env is_mod me in
+      let reso,_ = Safe_typing.delta_of_senv (Global.safe_env ()) in
+      include_subst env cur_mp reso mbids typ inl
+    with NoIncludeSelf -> empty_subst
+  in
+  let base_mp = get_module_path me in
+  let resolver = Global.add_include me is_mod inl in
+  let subst = join subst_self (map_mp base_mp cur_mp resolver) in
+  let aobjs = subst_aobjs subst aobjs in
+  ignore (Lib.add_leaf (Lib.current_mod_id ()) (in_include aobjs))
+
+let declare_include interp me_asts =
+  List.iter (declare_one_include interp) me_asts
+
+end
+
+
+(** {6 Module operations handling summary freeze/unfreeze} *)
 
 let protect_summaries f =
-  let fs = Summary.freeze_summaries () in
+  let fs = Summary.freeze_summaries ~marshallable:`No in
   try f fs
   with reraise ->
     (* Something wrong: undo the whole process *)
-    Summary.unfreeze_summaries fs; raise reraise
+    let reraise = Errors.push reraise in
+    let () = Summary.unfreeze_summaries fs in
+    iraise reraise
+
+let start_module interp export id args res =
+  protect_summaries (RawModOps.start_module interp export id args res)
 
-let declare_include interp_struct me_asts =
-  protect_summaries
-    (fun _ -> declare_include_ interp_struct me_asts)
+let end_module = RawModOps.end_module
 
-let declare_modtype interp_mt interp_mix id args mtys mty_l =
+let declare_module interp id args mtys me_l =
+  let declare_me fs = match me_l with
+    | [] -> RawModOps.declare_module interp id args mtys None fs
+    | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs
+    | me_l ->
+	ignore (RawModOps.start_module interp None id args mtys fs);
+	RawIncludeOps.declare_include interp me_l;
+	RawModOps.end_module ()
+  in
+  protect_summaries declare_me
+
+let start_modtype interp id args mtys =
+  protect_summaries (RawModTypeOps.start_modtype interp id args mtys)
+
+let end_modtype = RawModTypeOps.end_modtype
+
+let declare_modtype interp id args mtys mty_l =
   let declare_mt fs = match mty_l with
     | [] -> assert false
-    | [mty] -> declare_modtype_ interp_mt id args mtys mty fs
+    | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs
     | mty_l ->
-	ignore (start_modtype_ interp_mt id args mtys fs);
-	declare_include_ interp_mix mty_l;
-	end_modtype ()
+	ignore (RawModTypeOps.start_modtype interp id args mtys fs);
+	RawIncludeOps.declare_include interp mty_l;
+	RawModTypeOps.end_modtype ()
   in
   protect_summaries declare_mt
 
-let start_modtype interp_modtype id args mtys =
-  protect_summaries (start_modtype_ interp_modtype id args mtys)
+let declare_include interp me_asts =
+  protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts)
 
-let declare_module interp_mt interp_me interp_mix id args mtys me_l =
-  let declare_me fs = match me_l with
-    | [] -> declare_module_ interp_mt interp_me id args mtys None fs
-    | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs
-    | me_l ->
-	ignore (start_module_ interp_mt None id args mtys fs);
-	declare_include_ interp_mix me_l;
-	end_module ()
+
+(** {6 Libraries} *)
+
+type library_name = DirPath.t
+
+(** A library object is made of some substitutive objects
+    and some "keep" objects. *)
+
+type library_objects = Lib.lib_objects * Lib.lib_objects
+
+(** For the native compiler, we cache the library values *)
+
+type library_values = Nativecode.symbol array
+let library_values =
+  Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES"
+
+let register_library dir cenv (objs:library_objects) digest univ =
+  let mp = MPfile dir in
+  let () =
+    try
+      (* Is this library already loaded ? *)
+      ignore(Global.lookup_module mp);
+    with Not_found ->
+      (* If not, let's do it now ... *)
+      let mp', values = Global.import cenv univ digest in
+      if not (ModPath.equal mp mp') then
+        anomaly (Pp.str "Unexpected disk module name");
+      library_values := Dirmap.add dir values !library_values
   in
-  protect_summaries declare_me
+  let sobjs,keepobjs = objs in
+  do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
+
+let get_library_symbols_tbl dir = Dirmap.find dir !library_values
+
+let start_library dir =
+  let mp = Global.start_library dir in
+  openmod_info := default_module_info;
+  Lib.start_compilation dir mp;
+  Lib.add_frozen_state ()
+
+let end_library ?except dir =
+  let oname = Lib.end_compilation_checks dir in
+  let mp,cenv,ast = Global.export ?except dir in
+  let prefix, lib_stack = Lib.end_compilation oname in
+  assert (ModPath.equal mp (MPfile dir));
+  let substitute, keep, _ = Lib.classify_segment lib_stack in
+  cenv,(substitute,keep),ast
+
+
+
+(** {6 Implementation of Import and Export commands} *)
+
+let really_import_module mp =
+  (* May raise Not_found for unknown module and for functors *)
+  let prefix,sobjs,keepobjs = ModObjs.get mp in
+  Lib.open_objects 1 prefix sobjs;
+  Lib.open_objects 1 prefix keepobjs
+
+let cache_import (_,(_,mp)) = really_import_module mp
 
-let start_module interp_modtype export id args res =
- protect_summaries (start_module_ interp_modtype export id args res)
+let open_import i obj =
+  if Int.equal i 1 then cache_import obj
+
+let classify_import (export,_ as obj) =
+  if export then Substitute obj else Dispose
+
+let subst_import (subst,(export,mp as obj)) =
+  let mp' = subst_mp subst mp in
+  if mp'==mp then obj else (export,mp')
+
+let in_import : bool * module_path -> obj =
+  declare_object {(default_object "IMPORT MODULE") with
+    cache_function = cache_import;
+    open_function = open_import;
+    subst_function = subst_import;
+    classify_function = classify_import }
+
+let import_module export mp =
+  Lib.add_anonymous_leaf (in_import (export,mp))
 
 
-(*s Iterators. *)
+(** {6 Iterators} *)
 
 let iter_all_segments f =
-  let _ =
-    MPmap.iter
-      (fun _ (prefix,objects) ->
-	 let rec apply_obj (id,obj) = match object_tag obj with 
-	   | "INCLUDE" -> 
-	       let (_,(_,_,objs)) =  out_include obj in 
-		 List.iter apply_obj objs
-		   
-	   | _ -> f (make_oname prefix id) obj in
-	   List.iter apply_obj objects)
-      !modtab_objects
+  let rec apply_obj prefix (id,obj) = match object_tag obj with
+    | "INCLUDE" ->
+      let objs = expand_aobjs (out_include obj) in
+      List.iter (apply_obj prefix) objs
+    | _ -> f (make_oname prefix id) obj
   in
-  let rec apply_node = function
-    | sp, Leaf o -> f sp o
+  let apply_mod_obj _ (prefix,substobjs,keepobjs) =
+    List.iter (apply_obj prefix) substobjs;
+    List.iter (apply_obj prefix) keepobjs
+  in
+  let apply_node = function
+    | sp, Lib.Leaf o -> f sp o
     | _ -> ()
   in
-    List.iter apply_node (Lib.contents_after None)
+  MPmap.iter apply_mod_obj (ModObjs.all ());
+  List.iter apply_node (Lib.contents ())
+
+
+(** {6 Some types used to shorten declaremods.mli} *)
+
+type 'modast module_interpretor =
+  Environ.env -> Misctypes.module_kind -> 'modast ->
+    Entries.module_struct_entry * Misctypes.module_kind
+
+type 'modast module_params =
+  (Id.t Loc.located list * ('modast * inline)) list
+
 
+(** {6 Debug} *)
 
 let debug_print_modtab _ =
   let pr_seg = function
     | [] -> str "[]"
     | l -> str ("[." ^ string_of_int (List.length l) ^ ".]")
   in
-  let pr_modinfo mp (prefix,objects) s =
+  let pr_modinfo mp (prefix,substobjs,keepobjs) s =
     s ++ str (string_of_mp mp) ++ (spc ())
-    ++ (pr_seg (segment_of_objects prefix objects))
+    ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs)))
   in
-  let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in
-    hov 0 modules
+  let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in
+  hov 0 modules