- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des

  noms illégaux si le type auquel elle s'appliquait n'était pas pur ascii).
  [util.ml, termops.ml]
- Simplification de la procédure d'initialisation (apparemment des résidus
  obsolètes de la V5.10) et messages d'erreurs [lib.ml, toplevel.ml, coqtop.ml]
- Quelques pattern-matching incomplets [topconstr.ml, detyping.ml]


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

2 files changed, 6 insertions, 12 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index affe7f4e48..b9ca8bc8a3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -303,15 +303,9 @@ let parse_args is_ide =
       end
     | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end
 
-
-(* To prevent from doing the initialization twice *)
-let initialized = ref false
-
 let init is_ide =
-  if not !initialized then begin
-    initialized := true;
-    Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-    Lib.init();
+  Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+  begin
     try
       parse_args is_ide;
       re_exec is_ide;
@@ -328,10 +322,10 @@ let init is_ide =
       load_rcfile();
       load_vernacular ();
       compile_files ();
-      outputstate ();
+      outputstate ()
     with e ->
       flush_all();
-      if not !batch_mode then message "Error during initialization :";
+      if not !batch_mode then message "Error during initialization:";
       msgnl (Toplevel.print_toplevel_error e);
       exit 1
   end;
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 1ae8766336..cf3e1f54bb 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -140,12 +140,12 @@ let print_highlight_location ib loc =
 (* Functions to report located errors in a file. *)
 
 let print_location_in_file s inlibrary fname loc =
-  let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
+  let errstrm = (str"Error while reading " ++ str s ++ str":") in
   if loc = dummy_loc then 
     (errstrm ++ str", unknown location." ++ fnl ())
   else
     if inlibrary then
-      (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
+      (errstrm ++ fnl () ++ str"Module " ++ str ("\""^fname^"\"") ++
        str" characters " ++ Cerrors.print_loc loc ++ fnl ())
     else
     let (bp,ep) = unloc loc in