From 466c4cbacfb5ffb19ad9a042af7ab1f43441f925 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 17 Jul 2013 15:32:11 +0000 Subject: 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 --- library/libobject.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'library/libobject.mli') diff --git a/library/libobject.mli b/library/libobject.mli index fb38c4c3e..e886c4db0 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -45,7 +45,9 @@ open Mod_subst * a substitution function, performing the substitution; this function should be declared for substitutive objects - only (see above) + only (see above). NB: the substitution might now be delayed + instead of happening at module creation, so this function + should _not_ depend on the current environment * a discharge function, that is applied at section closing time to collect the data necessary to rebuild the discharged form of the -- cgit v1.2.3