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, 1 insertions, 1 deletions

diff --git a/printing/printmod.ml b/printing/printmod.ml
index 88880c293..ee4a2db7f 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -116,7 +116,7 @@ let nametab_register_module_body mp struc =
 
 let nametab_register_module_param mbid seb =
   (* For algebraic seb, we use a Declaremods function that converts into mse *)
-  try Declaremods.process_module_seb_binding mbid seb
+  try Declaremods.process_module_binding mbid seb
   with e when Errors.noncritical e ->
     (* Otherwise, for expanded structure, we try to play with the nametab *)
     match seb with