bug Reset et Sections

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

7 files changed, 27 insertions, 27 deletions

diff --git a/Makefile b/Makefile
index aba77cd8fc..2de7a99d7c 100644
--- a/Makefile
+++ b/Makefile
@@ -642,6 +642,9 @@ dependcoq: beforedepend
 
 ML4FILESML = $(ML4FILES:.ml4=.ml)
 
+ml4filesml:
+	$(MAKE) -f Makefile.dep $(ML4FILESML)
+
 depend: beforedepend
 # 1. We express dependencies of the .ml files w.r.t their grammars
 	rm -f .depend.camlp4
diff --git a/library/lib.ml b/library/lib.ml
index 53b5a21b04..10fd9b9655 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -160,7 +160,6 @@ let close_section export s =
   pop_path_prefix ();
   add_entry 
     (make_path (id_of_string s) OBJ) (ClosedSection (export, s,after'));
-  add_frozen_state ();
   (sp,after,fs)
 
 (* The following function exports the whole library segment, that will be 
diff --git a/library/lib.mli b/library/lib.mli
index bc4032a61d..668a65adf9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -28,6 +28,7 @@ and library_segment = library_entry list
 
 val add_leaf : identifier -> path_kind -> obj -> section_path
 val add_anonymous_leaf : obj -> unit
+val add_frozen_state : unit -> unit
 
 
 (*s The function [contents_after] returns the current library segment, 
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 9cafd5f7f3..d8f323d2f2 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -1,12 +1,9 @@
 
 (* $Id$ *)
 
-(* Ici, on trie la ligne de commande pour en extraire les options spécifiques
-   à coqmktop, puis on appelle "ocamlc" (ou "ocamlopt")
-   avec les autres options et la liste des fichiers à linker.
-
-   On essaye au maximum d'utiliser les modules Sys et Filename pour que la
-   portabilité soit maximale. *)
+(* coqmktop is a script to link Coq, analogous to ocamlmktop.
+   The command line contains options specific to coqmktop, options for the
+   Ocaml linker and files to link (in addition to the default Coq files). *)
 
 open Unix
 
@@ -99,8 +96,8 @@ let files_to_link userfiles =
   let modules = List.map module_of_file tolink in
   (modules, tolink)
 
-(*Gives the list of all the directories under dir*)
-(*Uses Unix, sorry... But you can try to do the same thing without it.*)
+(* Gives the list of all the directories under [dir].
+   Uses [Unix] (it is hard to do without it). *)
 let all_subdirs dir =
   let l = ref [] in
   let add f = l := f :: !l in
@@ -189,7 +186,7 @@ let clean file =
     rm (basename ^ ".cmx")
   end
 
-(*Gives all modules in dir. Uses .cmi. Unix again sorry again*)
+(* Gives all modules in [dir]. Uses [.cmi] suffixes. Uses [Unix]. *)
 let all_modules_in_dir dir =
   try
     let lst = ref []
@@ -207,16 +204,16 @@ let all_modules_in_dir dir =
   with Unix.Unix_error (_,"opendir",_) ->
     failwith ("all_modules_in_dir: directory "^dir^" not found")
 
-(*Gives a part of command line (corresponding to dir) for extract_crc*)
+(* Gives a part of command line (corresponding to dir) for [extract_crc] *)
 let crc_cmd dir =
   " -I "^dir^(List.fold_right (fun x y -> " "^x^y) (all_modules_in_dir dir)
   "")
 
-(*Same as crc_cmd but recursively*)
+(* Same as [crc_cmd] but recursively *)
 let rec_crc_cmd dir =
   List.fold_right (fun x y -> x^y) (List.map crc_cmd (all_subdirs dir)) ""
 
-(*Creates another temporary file for Dynlink if needed*)
+(* Creates another temporary file for Dynlink if needed *)
 let tmp_dynlink()=
   let tmp = Filename.temp_file "coqdynlink" ".ml" in
   let _ = Sys.command ("echo \"Dynlink.init();;\" > "^tmp) in
@@ -230,7 +227,7 @@ let tmp_dynlink()=
   in
   tmp
 
-(*Initializes the kind of loading in the main program*)
+(* Initializes the kind of loading in the main program *)
 let declare_loading_string () =
   if !opt then
     "Mltop.set Mltop.Native;;\n"
@@ -251,7 +248,7 @@ let create_tmp_main_file modules =
     output_string oc "List.iter Mltop.add_known_module [\"";
     output_string oc (String.concat "\";\"" modules);
     output_string oc "\"];;\n";
-    (*Initializes the kind of loading*)
+    (* Initializes the kind of loading *)
     output_string oc (declare_loading_string());
     (* Start the right toplevel loop: Coq or Coq_searchisos *)
     if !searchisos then 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3cc0bd5f40..64273724d5 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -7,9 +7,9 @@ open Toplevel
 
 let set_debug () = Options.debug := true
 
-(* Load of rcfile.
- * rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one
- * does not exist. *)
+(* Loading of the ressource file.
+   rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one
+  does not exist. *)
 
 let rcfile = ref (Filename.concat home ".coqrc")
 let rcfile_specified = ref false
@@ -31,11 +31,11 @@ let load_rcfile() =
       else if file_readable_p !rcfile then
         Vernac.load_vernac false !rcfile
       else ()
-(*
+	(*
 	if Options.is_verbose() then 
 	  mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^
 			 " found. Skipping rcfile loading.") >]
-*)
+	*)
     with e ->
       (mSGNL [< 'sTR"Load of rcfile failed." >];
        raise e)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 66c2e03010..41f266514d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -17,7 +17,7 @@ let memory_stat = ref false
 
 let print_memory_stat () = 
   if !memory_stat then
-    Format.printf "memory use = %d kbytes\n" (heap_size_kb ())
+    Format.printf "total heap size = %d kbytes\n" (heap_size_kb ())
 
 let _ = at_exit print_memory_stat
 
@@ -82,10 +82,9 @@ let re_exec s =
     Unix.execvp newprog Sys.argv
   end
 
-(* Parsing of the command line.
- *
- * We no longer use Arg.parse, in order to use share Usage.print_usage 
- * between coqtop and coqc. *)
+(*s Parsing of the command line.
+    We no longer use [Arg.parse], in order to use share [Usage.print_usage]
+    between coqtop and coqc. *)
 
 let usage () =
   if !batch_mode then
@@ -105,7 +104,7 @@ let parse_args () =
     | ("-I"|"-include") :: []       -> usage ()
 
     | "-R" :: d :: p :: rem -> set_rec_include d p; parse rem
-    | "-R" :: ([] | _ :: _) -> usage ()
+    | "-R" :: ([] | [_]) -> usage ()
 
     | "-q" :: rem -> no_load_rc (); parse rem
 
@@ -209,4 +208,4 @@ let start () =
   if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
   Toplevel.loop()
 
-(* Coqtop.start will be called by the code produced by coqmktop *)
+(* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 6712e900f8..5fce67d510 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -363,6 +363,7 @@ let close_section _ s =
   Summary.unfreeze_lost_summaries fs;
   let mc = segment_contents decls in
   add_anonymous_leaf (in_end_section (sec_sp,mc));
+  add_frozen_state ();
   if Options.immediate_discharge then ()
   else
     List.iter process_operation (List.rev ops)