Correction du bug 335 et Export/Require Export dans un module

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

4 files changed, 14 insertions, 7 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index d148a53435..5f2c068fdb 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -323,6 +323,6 @@ let close_section _ s =
       (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls 
   in
   let ids = last_section_hyps olddir in
-  Summary.unfreeze_lost_summaries fs;
+  Summary.section_unfreeze_summaries fs;
   catch_not_found (List.iter process_operation) (List.rev ops);
   Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e7402cbc63..f9d927f627 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -86,6 +86,7 @@ let _ =
     { freeze_function = Esyntax.freeze;
       unfreeze_function = Esyntax.unfreeze;
       init_function = Esyntax.init;
+      survive_module = false;
       survive_section = false }
 
 (* Pretty-printing objects = syntax_entry *)
@@ -121,6 +122,7 @@ let _ =
     { freeze_function = Egrammar.freeze;
       unfreeze_function = Egrammar.unfreeze;
       init_function = Egrammar.init;
+      survive_module = false;
       survive_section = false }
 
 (* Tokens *)
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index df40b6aa35..56d49d1bf4 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -249,6 +249,7 @@ let _ =
     { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules()));
       Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x);
       Summary.init_function = (fun () -> init_ml_modules ());
+      Summary.survive_module = false;
       Summary.survive_section = true }
 
 (* Same as restore_ml_modules, but verbosely *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index dc9b2663e5..9d20226b7a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -528,11 +528,15 @@ let vernac_require import _ qidl =
     else
       raise e
       
-let vernac_import export qidl =
-  let qidl = List.map qualid_of_reference qidl in
-  if export then
-    List.iter Library.export_library qidl
-  else
+let vernac_import export refl =
+  let import_one ref = 
+    let qid = qualid_of_reference ref in
+      Library.import_library export qid
+  in
+    List.iter import_one refl;
+    Lib.add_frozen_state ()
+
+(*  else
     let import (loc,qid) = 
       try
 	let mp = Nametab.locate_module qid in
@@ -543,7 +547,7 @@ let vernac_import export qidl =
 	 str ((string_of_qualid qid)^" is not a module"))
     in
       List.iter import qidl;
-      Lib.add_frozen_state ()
+*)
 
 let vernac_canonical locqid =
   Recordobj.objdef_declare (Nametab.global locqid)