module Library

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

16 files changed, 347 insertions, 124 deletions

diff --git a/.depend b/.depend
index 630144ee2..f6060aaf2 100644
--- a/.depend
+++ b/.depend
@@ -28,18 +28,17 @@ kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
 lib/util.cmi: lib/pp.cmi 
-library/global.cmi: kernel/constant.cmi kernel/evd.cmi kernel/inductive.cmi \
-    kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
+library/global.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi 
 library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi 
 library/libobject.cmi: kernel/names.cmi 
 library/summary.cmi: kernel/names.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
-parsing/g_minicoq.cmi: /usr/local/lib/camlp4/grammar.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi 
-parsing/lexer.cmi: /usr/local/lib/camlp4/token.cmi 
-parsing/pcoq.cmi: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
-    /usr/local/lib/camlp4/grammar.cmi /usr/local/lib/camlp4/token.cmi 
+parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+    kernel/term.cmi 
+parsing/pcoq.cmi: parsing/coqast.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
@@ -162,6 +161,10 @@ library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \
     library/libobject.cmi 
 library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \
     library/libobject.cmi 
+library/library.cmo: kernel/environ.cmi library/lib.cmi library/libobject.cmi \
+    kernel/names.cmi lib/system.cmi lib/util.cmi library/library.cmi 
+library/library.cmx: kernel/environ.cmx library/lib.cmx library/libobject.cmx \
+    kernel/names.cmx lib/system.cmx lib/util.cmx library/library.cmi 
 library/states.cmo: library/lib.cmi library/summary.cmi lib/system.cmi \
     library/states.cmi 
 library/states.cmx: library/lib.cmx library/summary.cmx lib/system.cmx \
@@ -171,11 +174,9 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
-    parsing/pcoq.cmi lib/pp.cmi /usr/local/lib/camlp4/stdpp.cmi lib/util.cmi \
-    parsing/ast.cmi 
+    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
-    parsing/pcoq.cmi lib/pp.cmx /usr/local/lib/camlp4/stdpp.cmi lib/util.cmx \
-    parsing/ast.cmi 
+    parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi 
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
@@ -187,54 +188,38 @@ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
     lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi 
 toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \
-    kernel/generic.cmi /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmi \
-    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
-    /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmi kernel/type_errors.cmi \
-    kernel/typing.cmi lib/util.cmi 
+    kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \
+    kernel/names.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/type_errors.cmi kernel/typing.cmi lib/util.cmi 
 toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \
-    kernel/generic.cmx /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmx \
-    kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
-    /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/type_errors.cmx \
-    kernel/typing.cmx lib/util.cmx 
-parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi 
-parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi 
-parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi 
-parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi 
-parsing/g_minicoq.cmo: kernel/generic.cmi /usr/local/lib/camlp4/gramext.cmi \
-    /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/generic.cmx toplevel/himsg.cmx kernel/inductive.cmx \
+    kernel/names.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/type_errors.cmx kernel/typing.cmx lib/util.cmx 
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \
+    lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
     parsing/g_minicoq.cmi 
-parsing/g_minicoq.cmx: kernel/generic.cmx /usr/local/lib/camlp4/gramext.cmi \
-    /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmx kernel/names.cmx \
-    lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \
+    lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     parsing/g_minicoq.cmi 
 parsing/g_multiple_case.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi 
-parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi 
-parsing/g_prim.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
-    parsing/pcoq.cmi 
-parsing/g_prim.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
     parsing/pcoq.cmi 
-parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi lib/pp.cmi 
-parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi lib/pp.cmx 
-parsing/g_vernac.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
-    parsing/pcoq.cmi 
-parsing/g_vernac.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
+parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \
     parsing/pcoq.cmi 
-parsing/pcoq.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
-    /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmi lib/pp.cmi \
+parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    lib/pp.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
+    lib/pp.cmx 
+parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
     lib/util.cmi parsing/pcoq.cmi 
-parsing/pcoq.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
-    /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmx lib/pp.cmx \
+parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
     lib/util.cmx parsing/pcoq.cmi 
-parsing/q_coqast.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/mLast.cmi \
-    parsing/pcoq.cmi /usr/local/lib/camlp4/quotation.cmi 
-parsing/q_coqast.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/mLast.cmi \
-    parsing/pcoq.cmi /usr/local/lib/camlp4/quotation.cmi 
+parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
diff --git a/Makefile b/Makefile
index 6ee0156d8..80d6cfc53 100644
--- a/Makefile
+++ b/Makefile
@@ -10,13 +10,13 @@ noargument:
 	@echo "   make cleanall"
 	@echo or make archclean
 
-INCLUDES=-I config -I lib -I kernel -I library -I parsing -I toplevel \
-	 -I $(CAMLP4LIB)
+LOCALINCLUDES=-I config -I lib -I kernel -I library -I parsing -I toplevel
+INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
 
 BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
 OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
 OCAMLDEP=ocamldep
-DEPFLAGS=$(INCLUDES)
+DEPFLAGS=$(LOCALINCLUDES)
 
 CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo
 OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
@@ -42,7 +42,7 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/typing.cmo
 
 LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
-	library/global.cmo library/states.cmo
+	library/global.cmo library/states.cmo library/library.cmo
 
 PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
diff --git a/configure b/configure
index 8da11ae6c..0cdd5f36a 100755
--- a/configure
+++ b/configure
@@ -237,15 +237,15 @@ esac
 
 # Objective Caml programs
 
-CAMLC=`which ocamlc`
+CAMLC=`which $bytecamlc`
 case $CAMLC in
-	"") echo "ocamlc is not present in your path !"
+	"") echo "$bytecamlc is not present in your path !"
 	echo "Give me manually the path to the ocamlc executable [/usr/local/bin by default]: "
 	read CAMLC
 	
 	case $CAMLC in
 		"") CAMLC=/usr/local/bin/ocamlc;;
-		*/ocamlc) true;;
+		*/ocamlc|*/ocamlc.opt) true;;
 		*/) CAMLC=${CAMLC}ocamlc;;
 		*) CAMLC=${CAMLC}/ocamlc;;
 	esac;;
diff --git a/dev/TODO b/dev/TODO
index 136ca5879..5a6e5b70e 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,11 +1,25 @@
 
- o Minicoq
-     utilisation de Himsg
+ o Univers
+     - définir un type d'ensemble de contraintes, et sauver cet ensemble
+	pour chaque module et non pas le graphe complet
+
+ o configure
+     - il faut tester la version du programme correspondant à $bytecamlc
+       qui peut être ocamlc ou ocamlc.opt, et non pas la version de "ocamlc"
+       seulement
+
+ o Environnements compilés (type Environ.compiled_env)
+     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
+
+ o Efficacité
+     - utiliser DOPL plutôt que DOPN (sauf pour Case)
+     - batch mode => pas de undo, ni de reset
+     - conversion : déplier la constante la plus récente
 
  o Lexer
      à compléter
 
  o Toplevel
      - boucle principale, affichage des erreur, du prompt
-     - parsing de la ligne de commande (Arg ?)
+     - parsing de la ligne de commande (utiliser Arg)
 
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 7cd127cf6..1fcf340f3 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -421,6 +421,8 @@ let add_mind sp mie env =
   in
   add_mind sp mib (set_universes (universes env_arities') env)
 
+let export = export
+let import = import
 
 (*s Machines with information. *)
 
diff --git a/kernel/typing.mli b/kernel/typing.mli
index d9d410c54..0167c8cd9 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -41,6 +41,9 @@ val lookup_mind : section_path -> 'a environment -> mutual_inductive_body
 val lookup_mind_specif : constr -> 'a environment -> mind_specif
 val lookup_meta : int -> 'a environment -> constr
 
+val export : 'a environment -> string -> compiled_env
+val import : compiled_env -> 'a environment -> 'a environment
+
 (*s Typing without information. *)
 
 type judgment
diff --git a/lib/system.ml b/lib/system.ml
index 016a6f97e..ab24f734c 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -46,33 +46,51 @@ let open_trapping_failure open_fun name suffix =
   let rname = make_suffix name suffix in
   try open_fun rname with _ -> error ("Can't open " ^ rname)
 
+let try_remove f =
+  try Sys.remove f
+  with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ;
+                     'sTR f ; 'sTR" which is corrupted !!" >]
+
+exception Bad_magic_number of string
+
+let (raw_extern_intern :
+     int -> string -> 
+       (string -> string * out_channel) * (string -> string * in_channel))
+  = fun magic suffix ->
+
+    let extern_state name = 
+      let (_,channel) as filec =
+	open_trapping_failure (fun n -> n,open_out_bin n) name suffix in
+      output_binary_int channel magic;
+      filec
+    and intern_state name = 
+      let fname = find_file_in_path (make_suffix name suffix) in
+      let channel = open_in_bin fname in
+      if input_binary_int channel <> magic then
+        raise (Bad_magic_number fname);
+      (fname,channel)
+    in 
+    (extern_state,intern_state)
+
 let (extern_intern :
-      int -> string -> ((string -> 'a -> unit) * (string -> 'a)))
+     int -> string -> (string -> 'a -> unit) * (string -> 'a))
   = fun magic suffix ->
 
-  let extern_state name val_0 = 
-    try
-      let (expname,channel) =
-        open_trapping_failure (fun n -> n,open_out_bin n) name suffix in
+    let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
+    let extern_state name val_0 = 
       try
-        output_binary_int channel magic;
-        output_value channel val_0;
-        close_out channel
-      with e -> begin
-        (try Sys.remove expname
-         with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ;
-                            'sTR expname ; 'sTR" which is corrupted !!" >]);
-        raise e
-      end
-    with Sys_error s -> error ("System error: " ^ s)
+	let (fname,channel) = raw_extern name in
+      	try
+          output_value channel val_0;
+          close_out channel
+      	with e -> 
+	  begin try_remove fname; raise e end
+      with Sys_error s -> error ("System error: " ^ s)
 
   and intern_state name = 
     try
-      let fname = find_file_in_path (make_suffix name suffix) in
-      let channel = open_in_bin fname in
-      if input_binary_int channel <> magic then
-        error (fname^" not compiled with the current version of Coq");
-      let v = input_value(channel) in
+      let (fname,channel) = raw_intern name in
+      let v = input_value channel in
       close_in channel; 
       v
     with Sys_error s -> error("System error: " ^ s)
diff --git a/lib/system.mli b/lib/system.mli
index b887f5eb5..f89e128cb 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,6 +6,17 @@
 val add_path : string -> unit
 val del_path : string -> unit
 
+val find_file_in_path : string -> string
+
+(*s Generic input and output functions, parameterized by a magic number
+  and a suffix. The intern functions raise the exception [Bad_magic_number]
+  when the check fails, with the full file name. *)
+
+exception Bad_magic_number of string
+
+val raw_extern_intern : int -> string -> 
+  (string -> string * out_channel) * (string -> string * in_channel)
+
 val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a)
 
 (*s Time stamps. *)
diff --git a/library/global.ml b/library/global.ml
index d669410b8..d7267a96d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -35,3 +35,5 @@ let lookup_mind sp = lookup_mind sp !global_env
 let lookup_mind_specif c = lookup_mind_specif c !global_env
 let lookup_meta n = lookup_meta n !global_env
 
+let export s = export !global_env s
+let import cenv = global_env := import cenv !global_env
diff --git a/library/global.mli b/library/global.mli
index 4f04d2e51..d21509e32 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -9,6 +9,7 @@ open Sign
 open Evd
 open Constant
 open Inductive
+open Environ
 (*i*)
 
 (* This module defines the global environment of Coq. 
@@ -33,3 +34,5 @@ val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : constr -> mind_specif
 val lookup_meta : int -> constr
 
+val export : string -> compiled_env
+val import : compiled_env -> unit
diff --git a/library/lib.ml b/library/lib.ml
index a8ab156c5..42850bc05 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -20,7 +20,11 @@ type library_entry = section_path * node
 
 
 (* We keep trace of operations in a stack [lib_stk]. 
-   [path_prefix] is the current path of sections (in correct order). *)
+   [path_prefix] is the current path of sections. Sections are stored in 
+   ``correct'' order, the oldest coming first in the list. It may seems 
+   costly, but in practice there is not so many openings and closings of
+   sections, but on the contrary there are many constructions of section
+   paths. *) 
 
 let lib_stk = ref ([] : (section_path * node) list)
 
@@ -122,7 +126,7 @@ let close_section s =
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
-  add_entry sp (ClosedSection (s,modp,after));
+  add_entry sp (ClosedSection (s,modp,List.rev after));
   add_frozen_state ();
   pop_path_prefix ()
 
diff --git a/library/lib.mli b/library/lib.mli
index 80f61ef40..a38fb4cef 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -25,7 +25,7 @@ type library_entry = section_path * node
 
 
 (*s Adding operations, and getting the current list of operations (most 
-  recent ones come first). *)
+  recent ones coming first). *)
 
 val add_leaf : identifier -> obj -> section_path
 val add_anonymous_leaf : obj -> unit
@@ -33,7 +33,8 @@ val add_anonymous_leaf : obj -> unit
 val contents_after : section_path option -> library_segment
 
 
-(*s Opening and closing a section. *)
+(*s Opening and closing a section. The boolean in [open_section] indicates
+  a module. *)
 
 val open_section : string -> bool -> section_path
 val close_section : string -> unit
diff --git a/library/libobject.ml b/library/libobject.ml
index f5e610704..1096ac43a 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -5,15 +5,17 @@ open Util
 open Names
 
 type 'a object_declaration = {
-  load_function : 'a -> unit;
   cache_function : section_path * 'a -> unit;
+  load_function : 'a -> unit;
+  open_function : 'a -> unit;
   specification_function : 'a -> 'a }
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
 type dynamic_object_declaration = {
-  dyn_load_function : obj -> unit;
   dyn_cache_function : section_path * obj -> unit;
+  dyn_load_function : obj -> unit;
+  dyn_open_function : obj -> unit;
   dyn_specification_function : obj -> obj }
 
 let object_tag lobj = Dyn.tag lobj
@@ -23,41 +25,39 @@ let cache_tab =
 
 let declare_object (na,odecl) =
   let (infun,outfun) = Dyn.create na in
-  let loader lobj =
-    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the loadfun"
-  and cacher (spopt,lobj) =
+  let cacher (spopt,lobj) =
     if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the cachefun"
+  and loader lobj =
+    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the loadfun"
+  and opener lobj =
+    if Dyn.tag lobj = na then odecl.open_function (outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the openfun"
   and spec_extractor lobj = 
     infun(odecl.specification_function (outfun lobj))
   in 
-  Hashtbl.add cache_tab na { dyn_load_function = loader;
-                             dyn_cache_function = cacher;
+  Hashtbl.add cache_tab na { dyn_cache_function = cacher;
+			     dyn_load_function = loader;
+                             dyn_open_function = opener;
                              dyn_specification_function = spec_extractor };
   (infun,outfun)
 
-
-let load_object lobj =
+let apply_dyn_fun f lobj =
   let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in 
-    dodecl.dyn_load_function lobj
-  with Not_found ->
-    anomaly ("Cannot find loadfun for an object with tag "^tag)
+  try
+    let dodecl = Hashtbl.find cache_tab tag in f dodecl
+  with Not_found -> 
+    anomaly ("Cannot find library functions for an object with tag "^tag)
 
-let cache_object (spopt,lobj) =
-  let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in 
-    dodecl.dyn_cache_function(spopt,lobj)
-  with Not_found ->
-    anomaly ("Cannot find cachefun for an object with tag "^tag)
+let cache_object ((_,lobj) as node) =
+  apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
+
+let load_object lobj = 
+  apply_dyn_fun (fun d -> d.dyn_load_function lobj) lobj
+
+let open_object lobj = 
+  apply_dyn_fun (fun d -> d.dyn_open_function lobj) lobj
 
 let extract_object_specification lobj =
-  let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in
-    dodecl.dyn_specification_function lobj
-  with Not_found ->
-    anomaly ("Cannot find specification extractor for an object with tag "^tag)
+  apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 967e4c410..7ddac57b2 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -5,20 +5,23 @@
 open Names
 (*i*)
 
-(* [Libobject] declares persistent objects given with three methods:
+(* [Libobject] declares persistent objects, given with three methods:
+   - a caching function specifying how to add the object in the current
+     scope of theory modules;
    - a loading function, specifying what to do when the object is loaded
      from the disk;
-   - a caching function specifying how to import the object in the current
-     scope of theory modules;
+   - an opening function, specifying what to do when the module containing
+     the object is opened;
    - a specification function, to extract its specification when writing
      the specification of a module to the disk (.vi) *)
 
 type 'a object_declaration = {
-  load_function : 'a -> unit;
   cache_function : section_path * 'a -> unit;
+  load_function : 'a -> unit;
+  open_function : 'a -> unit;
   specification_function : 'a -> 'a }
 
-(*s given the object-name, the "loading" function, the "caching" function, 
+(*s Given the object-name, the "loading" function, the "caching" function, 
    and the "specification" function, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
@@ -30,8 +33,7 @@ val declare_object :
 
 val object_tag : obj -> string
 
-val load_object : obj -> unit
-
 val cache_object : (section_path * obj) -> unit
-
+val load_object : obj -> unit
+val open_object : obj -> unit
 val extract_object_specification : obj -> obj
diff --git a/library/library.ml b/library/library.ml
new file mode 100644
index 000000000..7de5a845d
--- /dev/null
+++ b/library/library.ml
@@ -0,0 +1,150 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Environ
+open Libobject
+open Lib
+
+(* Modules on disk contain the following informations (after the magic 
+   number, and before the digest). *)
+
+type module_disk = { 
+  md_name : string;
+  md_compiled_env : compiled_env;
+  md_declarations : library_segment;
+  md_deps : (string * Digest.t * bool) list }
+
+(* Modules loaded in memory contain the following informations. They are
+   kept in the hash table [modules_table]. *)
+
+type module_t = {
+  module_name : string;
+  module_compiled_env : compiled_env;
+  module_declarations : library_segment;
+  mutable module_opened : bool;
+  mutable module_exported : bool;
+  module_deps : (string * Digest.t * bool) list;
+  module_digest : Digest.t }
+
+let modules_table =
+  (Hashtbl.create 17 : (string, module_t) Hashtbl.t)
+
+let find_module s =
+  try
+    Hashtbl.find modules_table s
+  with Not_found ->
+    error ("Unknown module " ^ s)
+
+let module_is_loaded s =
+  try let _ = Hashtbl.find modules_table s in true with Not_found -> false
+
+let module_is_opened s =
+  (find_module s).module_opened
+
+let vo_magic_number = 0700
+
+let (raw_extern_module, raw_intern_module) =
+  System.raw_extern_intern vo_magic_number ".vo"
+
+let segment_iter f =
+  let rec apply = function
+    | _,Leaf obj -> f obj
+    | _,ClosedSection (_,_,mseg) -> iter mseg
+    | _,OpenedSection _ -> assert false
+    | _,FrozenState _ -> ()
+  and iter seg =
+    List.iter apply seg
+  in
+  iter
+
+
+(* [open_module s] opens a module which is assumed to be already loaded. *)
+
+let open_module s =
+  let m = find_module s in
+  if not m.module_opened then begin
+    segment_iter open_object m.module_declarations;
+    m.module_opened <- true
+  end
+
+
+(* [load_module s] loads the module [s] from the disk, and [find_module s]
+   returns the module of name [s], loading it if necessary. 
+   The boolean [doexp] specifies if we open the modules which are declared
+   exported in the dependencies (usually it is [true] at the highest level;
+   it is always [false] in recursive loadings). *)
+
+let load_objects s =
+  let m = find_module s in
+  segment_iter load_object m.module_declarations
+
+let rec load_module_from doexp s f =
+  let (fname,ch) = raw_intern_module f in
+  let md = input_value ch in
+  let digest = input_value ch in
+  close_in ch;
+  let m = { module_name = md.md_name;
+	    module_compiled_env = md.md_compiled_env;
+	    module_declarations = md.md_declarations;
+	    module_opened = false;
+	    module_exported = false;
+	    module_deps = md.md_deps;
+	    module_digest = digest } in
+  if s <> md.md_name then
+    error ("The file " ^ fname ^ " does not contain module " ^ s);
+  List.iter (load_mandatory_module doexp s) m.module_deps;
+  Hashtbl.add modules_table s m;
+  m
+
+and load_mandatory_module doexp caller (s,d,export) =
+  let m = find_module false s s in
+  if d <> m.module_digest then
+    error ("module "^caller^" makes inconsistent assumptions over module "^s);
+  if doexp && export then open_module s
+
+and find_module doexp s f =
+  try Hashtbl.find modules_table s with Not_found -> load_module_from doexp s f
+
+
+let load_module s = function
+  | None -> let _ = load_module_from true s s in ()
+  | Some f -> let _ = load_module_from true s f in ()
+
+
+(* [require_module] loads and opens a module. *)
+
+let require_module spec name fileopt export =
+  let file = match fileopt with
+    | None -> name
+    | Some f -> f in
+  let m = load_module_from true name file in
+  open_module name;
+  if export then m.module_exported <- true
+
+
+(* [save_module s] saves the module [m] to the disk. *)
+
+let current_imports () =
+  let l = ref [] in
+  Hashtbl.iter 
+    (fun _ m -> l := (m.module_name, m.module_digest, m.module_exported) :: !l)
+    modules_table;
+  !l
+
+let save_module_to s f =
+  let seg = contents_after None in
+  let md = { 
+    md_name = s;
+    md_compiled_env = Global.export s;
+    md_declarations = seg;
+    md_deps = current_imports () } in
+  let (_,ch) = raw_extern_module f in
+  output_value ch md;
+  flush ch;
+  let di = Digest.file f in
+  output_value ch di;
+  close_out ch
+
+
diff --git a/library/library.mli b/library/library.mli
new file mode 100644
index 000000000..2c54aec2e
--- /dev/null
+++ b/library/library.mli
@@ -0,0 +1,28 @@
+
+(* $Id$ *)
+
+(* This module is the heart of the library. It provides low level functions to
+   load, open and save modules. Modules are saved onto the disk with checksums
+   (obtained with the [Digest] module), which are checked at loading time to
+   prevent inconsistencies between files written at various dates. It also
+   provides a high level function [require] which corresponds to the 
+   vernacular command [Require]. *)
+
+val load_module : string -> string option -> unit
+val open_module : string -> unit
+
+val module_is_loaded : string -> bool
+val module_is_opened : string -> bool
+
+(*s Require. The command [require_module spec m file export] loads and opens
+  a module [m]. [file] specifies the filename, if not [None]. [spec]
+  specifies to look for a specification ([true]) or for an implementation
+  ([false]), if not [None]. And [export] specifies if the module must be 
+  exported. *)
+
+val require_module : bool option -> string -> string option -> bool -> unit
+
+(*s [save_module_to s f] saves the current environment as a module [s]
+  in the file [f]. *)
+
+val save_module_to : string -> string -> unit