Declaremods: major refactoring, stop duplicating libobjects in modules

 When refering to a module / module type, or when doing an include,
 we do not duplicate and substitution original libobjects immediatly.
 Instead, we store the module path, plus a substitution. The libobjects
 are retrieved later from this module path and substituted, typically
 during a Require. This allows to vastly decrease vo size (up to 50%
 on some files in the stdlib). More work is done during load (some
 substitutions), but the extra time overhead appears to be negligible.

 Beware: all subst_function operations should now be
 environment-insensitive, since they may be arbitrarily delayed.
 Apparently only subst_arguments_scope had to be adapted.

 A few more remarks:

 - Increased code factorisation between modules and modtypes
 - Many errors and anomaly are now assert
 - One hack : brutal access of inner parts of module types
   (cf handle_missing_substobjs)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 14 deletions

diff --git a/interp/modintern.mli b/interp/modintern.mli
index e76deb33d6..b6128918c1 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -14,6 +14,7 @@ open Pp
 open Libnames
 open Names
 open Constrexpr
+open Misctypes
 
 (** Module internalization errors *)
 
@@ -25,17 +26,11 @@ type module_internalization_error =
 exception ModuleInternalizationError of module_internalization_error
 
 (** Module expressions and module types are interpreted relatively to
-   possible functor or functor signature arguments. *)
-
-val interp_modtype : env -> module_ast -> module_struct_entry
-
-val interp_modexpr : env -> module_ast -> module_struct_entry
-
-(** The following function tries to interprete an ast as a module,
-   and in case of failure, interpretes this ast as a module type.
-   The boolean is true for a module, false for a module type *)
-
-val interp_modexpr_or_modtype : env -> module_ast ->
- module_struct_entry * bool
-
-val lookup_module : qualid located -> module_path
+   possible functor or functor signature arguments. When the input kind
+   is ModAny (i.e. module or module type), we tries to interprete this ast
+   as a module, and in case of failure, as a module type. The returned
+   kind is never ModAny, and it is equal to the input kind when this one
+   isn't ModAny. *)
+
+val interp_module_ast :
+  env -> module_kind -> module_ast -> module_struct_entry * module_kind