corrections mineures suite au commit de restructuration du noyau

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

5 files changed, 29 insertions, 30 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 1f5b69458..9fa7b1477 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -229,7 +229,7 @@ let declare_constant id cd =
   sp
 
 let redeclare_constant sp cd =
-  add_absolutely_named_lead sp (in_constant cd);
+  add_absolutely_named_leaf sp (in_constant cd);
   if is_implicit_args() then declare_constant_implicits sp
 
 (* Inductives. *)
diff --git a/library/impargs.ml b/library/impargs.ml
index fec4df020..d6a7859a9 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -351,7 +351,7 @@ let _ =
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
-      Summary.survive_section = true }
+      Summary.survive_section = false }
 
 let rollback f x =
   let fs = freeze () in
diff --git a/library/lib.ml b/library/lib.ml
index cd71de3a3..17b8fa8da 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -38,7 +38,6 @@ and library_segment = library_entry list
 
 let lib_stk = ref ([] : (section_path * node) list)
 
-
 let module_name = ref None
 let path_prefix = ref (default_module : dir_path)
 
@@ -92,7 +91,7 @@ let add_anonymous_entry node =
   add_entry sp node;
   sp
 
-let add_absolutely_named_lead sp obj =
+let add_absolutely_named_leaf sp obj =
   cache_object (sp,obj);
   add_entry sp (Leaf obj)
 
@@ -114,18 +113,7 @@ let contents_after = function
   | None -> !lib_stk
   | Some sp -> let (after,_,_) = split_lib sp in after
 
-(* Sections. *)
-
-let open_section id =
-  let dir = extend_dirpath !path_prefix id in
-  let sp = make_path id in
-  if Nametab.exists_section dir then
-    errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
-  add_entry sp (OpenedSection (dir, freeze_summaries()));
-  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-  Nametab.push_section dir;
-  path_prefix := dir;
-  sp
+(* Modules. *)
 
 let check_for_module () =
   let is_decl = function (_,FrozenState _) -> false | _ -> true in
@@ -134,6 +122,7 @@ let check_for_module () =
     error "a module can not be started after some declarations"
   with Not_found -> ()
 
+(* TODO: use check_for_module ? *)
 let start_module s =
   if !module_name <> None then
     error "a module is already started";
@@ -153,6 +142,20 @@ let end_module s =
 	  error ("The current open module has basename "^(string_of_id bm));
 	m
 
+(* Sections. *)
+
+let open_section id =
+  let dir = extend_dirpath !path_prefix id in
+  let sp = make_path id in
+  if Nametab.exists_section dir then
+    errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
+  let sum = freeze_summaries() in
+  add_entry sp (OpenedSection (dir, sum));
+  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+  Nametab.push_section dir;
+  path_prefix := dir;
+  sp
+
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
 let sections_are_opened () =
@@ -172,6 +175,8 @@ let export_segment seg =
   in
   clean [] seg
 
+(* Restore lib_stk and summaries as before the section opening, and
+   add a ClosedSection object. *)
 let close_section export id =
   let sp,dir,fs = 
     try match find_entry_p is_opened_section with
@@ -185,9 +190,9 @@ let close_section export id =
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
-  let after' = export_segment after in
   pop_path_prefix ();
-  add_entry (make_path id) (ClosedSection (export, dir, after'));
+  let closed_sec = ClosedSection (export, dir, export_segment after) in
+  add_entry (make_path id) closed_sec;
   (dir,after,fs)
 
 (* The following function exports the whole library segment, that will be 
diff --git a/library/lib.mli b/library/lib.mli
index 832e6cff9..f335d48ad 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -34,7 +34,7 @@ and library_segment = library_entry list
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : identifier -> obj -> section_path
-val add_absolutely_named_lead : section_path -> obj -> unit
+val add_absolutely_named_leaf : section_path -> obj -> unit
 val add_anonymous_leaf : obj -> unit
 val add_frozen_state : unit -> unit
 
diff --git a/library/states.ml b/library/states.ml
index 6bd8b7d64..9b1068a2b 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -9,17 +9,15 @@
 (* $Id$ *)
 
 open System
-open Lib
-open Summary
 
 type state = Lib.frozen * Summary.frozen
 
 let get_state () =
-  (Lib.freeze(), freeze_summaries())
+  (Lib.freeze(), Summary.freeze_summaries())
 
 let set_state (fl,fs) =
   Lib.unfreeze fl;
-  unfreeze_summaries fs
+  Summary.unfreeze_summaries fs
 
 let state_magic_number = 19764
 
@@ -34,12 +32,8 @@ let freeze = get_state
 let unfreeze = set_state
 
 let with_heavy_rollback f x =
-  let sum = freeze_summaries ()
-  and flib = freeze() in
+  let st = get_state () in
   try 
     f x
-  with reraise -> begin
-    unfreeze_summaries sum;
-    unfreeze flib;
-    raise reraise
-  end
+  with reraise ->
+    (set_state st; raise reraise)