diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-17 15:32:11 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-17 15:32:11 +0000 |
commit | 466c4cbacfb5ffb19ad9a042af7ab1f43441f925 (patch) | |
tree | d53d87c5ac811f19056715d6ec3f2a98d5675ece /checker/values.ml | |
parent | 8741623408e100097167504bc35c4cbb7982aedd (diff) |
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
Diffstat (limited to 'checker/values.ml')
-rw-r--r-- | checker/values.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml index b05085ae4..0855263f7 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -280,7 +280,7 @@ let v_compiled_lib = let v_obj = Tuple ("Dyn.t",[|String;Any|]) let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) let v_libobjs = List v_libobj -let v_libraryobjs = Tuple ("library_objects",[|v_mp;v_libobjs;v_libobjs|]) +let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) (** Toplevel structures in a vo (see Cic.mli) *) |