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
---
 checker/values.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/values.ml b/checker/values.ml
index b05085ae44..0855263f7a 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) *)
 
-- 
cgit v1.2.3