aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-30 07:56:49 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-30 07:56:49 +0200
commit5383cdc276d9ba7f1bb05bfe5aeae0a25edbd4a4 (patch)
tree314bbbcdf4b932bf98de14c19831ac4e5cfc8ee5
parent9a5fb78ef3c7c5d4f568a4d04e169475e9105def (diff)
Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.
"This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
-rw-r--r--tools/coq_makefile.ml4
-rw-r--r--tools/coq_tex.ml4
-rw-r--r--tools/coqdep_boot.ml4
-rw-r--r--tools/coqdoc/main.ml4
-rw-r--r--tools/coqwc.mll4
-rw-r--r--tools/gallina.ml5
6 files changed, 6 insertions, 19 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 8f4772e28..71134c2d9 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -842,11 +842,9 @@ let do_makefile args =
if not (makefile = None) then close_out !output_channel;
exit 0
-let main () =
+let _ =
let args =
if Array.length Sys.argv = 1 then usage ();
List.tl (Array.to_list Sys.argv)
in
do_makefile args
-
-let _ = Printexc.catch main ()
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index f65708698..53444cee7 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -285,7 +285,7 @@ let find_coqtop () =
"coqtop"
end
-let main () =
+let _ =
parse_cl ();
if !image = "" then image := Filename.quote (find_coqtop ());
if !boot then image := !image ^ " -boot";
@@ -298,5 +298,3 @@ let main () =
flush stdout
end;
List.iter one_file (List.rev !files)
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 2d5fd36a6..64ce66d2d 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -30,7 +30,7 @@ let rec parse = function
| f :: ll -> treat_file None f; parse ll
| [] -> ()
-let coqdep_boot () =
+let _ =
let () = option_boot := true in
if Array.length Sys.argv < 2 then exit 1;
parse (List.tl (Array.to_list Sys.argv));
@@ -47,5 +47,3 @@ let coqdep_boot () =
end;
if !option_c then mL_dependencies ();
coq_dependencies ()
-
-let _ = Printexc.catch coqdep_boot ()
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 9531cd2b0..2554ed495 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -557,10 +557,8 @@ let produce_output fl =
(*s \textbf{Main program.} Print the banner, parse the command line,
read the files and then call [produce_document] from module [Web]. *)
-let main () =
+let _ =
let files = parse () in
Index.init_coqlib_library ();
if not !quiet then banner ();
if files <> [] then produce_output files
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 417ec5355..9a42553da 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -276,7 +276,7 @@ let rec parse = function
(*s Main program. *)
-let main () =
+let _ =
let files = parse (List.tl (Array.to_list Sys.argv)) in
if not (!spec_only || !proof_only) then
printf " spec proof comments\n";
@@ -285,8 +285,6 @@ let main () =
| [f] -> process_file f
| _ -> List.iter process_file files; print_totals ()
-let _ = Printexc.catch main ()
-
(*i*)}(*i*)
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 279919c58..5ce19e7f8 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -39,7 +39,7 @@ let traite_stdin () =
with Sys_error _ ->
()
-let gallina () =
+let _ =
let lg_command = Array.length Sys.argv in
if lg_command < 2 then begin
output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
@@ -59,6 +59,3 @@ let gallina () =
traite_stdin ()
else
List.iter traite_fichier !vfiles
-
-let _ = Printexc.catch gallina ()
-