Error_in_file redondant et inapproprié

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

1 files changed, 16 insertions, 20 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e28821268..ed2c3c154 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -101,8 +101,7 @@ let rec vernac interpfun input =
   let (loc,com) = parse_phrase input in
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
-        let _ = read_vernac_file verbosely (make_suffix fname ".v") in
-        ()
+        read_vernac_file verbosely (make_suffix fname ".v")
 
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
 
@@ -132,11 +131,11 @@ and read_vernac_file verbosely s =
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
-    while true do vernac interpfun input; pp_flush () done; fname
+    while true do vernac interpfun input; pp_flush () done
   with e ->   (* whatever the exception *)
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
-      | End_of_input -> fname
+      | End_of_input -> ()
       | _ -> raise_with_file fname e
 
 (* raw_do_vernac : char Stream.t -> unit
@@ -151,24 +150,21 @@ let raw_do_vernac po =
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   try 
-    let _ = read_vernac_file verb file in ()
+    read_vernac_file verb file
   with e -> 
     raise_with_file file e
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
-  try
-    let s = Filename.basename f in
-    let m = Names.id_of_string s in
-    let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
-    let ldir0 = Library.find_logical_path (Filename.dirname longf) in
-    let ldir = Nameops.extend_dirpath ldir0 m in
-    Termops.set_module ldir; (* Just for universe naming *)
-    Lib.start_module ldir;
-    if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
-    let _ = load_vernac verbosely longf in
-    let mid = Lib.end_module m in
-    assert (mid = ldir);
-    Library.save_module_to ldir (longf^"o")
-  with e ->
-    raise_with_file f e
+  let s = Filename.basename f in
+  let m = Names.id_of_string s in
+  let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
+  let ldir0 = Library.find_logical_path (Filename.dirname longf) in
+  let ldir = Nameops.extend_dirpath ldir0 m in
+  Termops.set_module ldir; (* Just for universe naming *)
+  Lib.start_module ldir;
+  if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+  let _ = load_vernac verbosely longf in
+  let mid = Lib.end_module m in
+  assert (mid = ldir);
+  Library.save_module_to ldir (longf^"o")