2 files changed, 21 insertions, 25 deletions
diff --git a/checker/check.ml b/checker/check.ml
index c3f0e976fc..88306e2148 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -234,28 +234,29 @@ let locate_qualified_library qid =
       (dir, file)
   with Not_found -> raise LibNotFound
 
-let explain_locate_library_error qid = function
-  | LibUnmappedDir ->
-      let prefix = qid.dirpath in
-      errorlabstrm "load_absolute_library_from"
-      (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
-      str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
-  | LibNotFound ->
-      errorlabstrm "load_absolute_library_from"
-      (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
-  | e -> raise e
+let error_unmapped_dir qid =
+  let prefix = qid.dirpath in
+  errorlabstrm "load_absolute_library_from"
+    (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
+     str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
+
+let error_lib_not_found qid =
+  errorlabstrm "load_absolute_library_from"
+    (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
 
 let try_locate_absolute_library dir =
   try
     locate_absolute_library dir
-  with e ->
-    explain_locate_library_error (path_of_dirpath dir) e
+  with
+    | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir)
+    | LibNotFound -> error_lib_not_found (path_of_dirpath dir)
 
 let try_locate_qualified_library qid =
   try
     locate_qualified_library qid
-  with e ->
-    explain_locate_library_error qid e
+  with
+    | LibUnmappedDir -> error_unmapped_dir qid
+    | LibNotFound -> error_lib_not_found qid
 
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
diff --git a/checker/checker.ml b/checker/checker.ml
index 9834b1331a..10a3089ed7 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -70,8 +70,9 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
 
 let convert_string d =
   try Id.of_string d
-  with _ ->
-    if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+  with Errors.UserError _ ->
+    if_verbose msg_warning
+      (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
     raise Exit
 
 let add_rec_path ~unix_path ~coq_root =
@@ -279,9 +280,9 @@ let rec explain_exn = function
 	       report ())
   | e when is_anomaly e ->
       print_anomaly e
-  | reraise ->
+  | e ->
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
-	       str (Printexc.to_string reraise)++report())
+	       str (Printexc.to_string e)++report())
 
 let parse_args argv =
   let rec parse = function
@@ -334,13 +335,7 @@ let parse_args argv =
         fatal_error (str "Unknown option " ++ str s)
     | s :: rem ->  add_compile s; parse rem
   in
-  try
-    parse (List.tl (Array.to_list argv))
-  with
-    | UserError(_, s) as e ->
-      if Pp.is_empty s then exit 1
-      else fatal_error (explain_exn e)
-    | e -> begin fatal_error (explain_exn e) end
+  parse (List.tl (Array.to_list argv))
 
 
 (* To prevent from doing the initialization twice *)