1 files changed, 18 insertions, 30 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 825fb4dc..8dbb7e01 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open System
 open Flags
@@ -16,8 +16,10 @@ open Check
 
 let () = at_exit flush_all
 
+let chk_pp = Pp.pp_with Format.std_formatter
+
 let fatal_error info anomaly =
-  flush_all (); pperrnl info; flush_all ();
+  flush_all (); Feedback.msg_error info; flush_all ();
   exit (if anomaly then 129 else 1)
 
 let coq_root = Id.of_string "Coq"
@@ -67,12 +69,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
       Check.add_load_path (dir,coq_dirpath)
     end
   else
-    msg_warning (str "Cannot open " ++ str dir)
+    Feedback.msg_warning (str "Cannot open " ++ str dir)
 
 let convert_string d =
   try Id.of_string d
-  with Errors.UserError _ ->
-    if_verbose msg_warning
+  with CErrors.UserError _ ->
+    if_verbose Feedback.msg_warning
       (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
@@ -90,7 +92,7 @@ let add_rec_path ~unix_path ~coq_root =
     List.iter Check.add_load_path dirs;
     Check.add_load_path (unix_path, coq_root)
   else
-    msg_warning (str "Cannot open " ++ str unix_path)
+    Feedback.msg_warning (str "Cannot open " ++ str unix_path)
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -123,7 +125,7 @@ let init_load_path () =
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
   (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
-    (xdg_dirs ~warn:(fun x -> msg_warning (str x)));
+    (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)));
   (* then directories in COQPATH *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
   (* then current directory *)
@@ -140,9 +142,7 @@ let set_debug () = Flags.debug := true
 
 let impredicative_set = ref Cic.PredicativeSet
 let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
-let type_in_type = ref Cic.StratifiedType
-let set_type_in_type () = type_in_type := Cic.TypeInType
-let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
+let engage () = Safe_typing.set_engagement (!impredicative_set)
 
 
 let admit_list = ref ([] : section_path list)
@@ -179,10 +179,7 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "coqchk options are:\n";
   output_string co
-"  -I dir -as coqdir      map physical dir to logical coqdir\
-\n  -I dir                 map directory dir to the empty logical path\
-\n  -include dir           (idem)\
-\n  -R dir coqdir          recursively map physical dir to logical coqdir\
+"  -R dir coqdir          map physical dir to logical coqdir\
 \n\
 \n  -admit module          load module and dependencies without checking\
 \n  -norec module          check module but admit dependencies without checking\
@@ -195,7 +192,6 @@ let print_usage_channel co command =
 \n  -silent                disable trace of constants being checked\
 \n\
 \n  -impredicative-set     set sort Set impredicative\
-\n  -type-in-type          collapse type hierarchy\
 \n\
 \n  -h, --help             print this list of options\
 \n"
@@ -215,14 +211,9 @@ let usage () =
 open Type_errors
 
 let anomaly_string () = str "Anomaly: "
-let report () = (str "." ++ spc () ++ str "Please report.")
+let report () = (str "." ++ spc () ++ str "Please report" ++
+                 strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".")
 
-let print_loc loc =
-  if loc = Loc.ghost then
-    (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    (int (fst loc) ++ str"-" ++ int (snd loc))
 let guill s = str "\"" ++ str s ++ str "\""
 
 let where s =
@@ -294,7 +285,8 @@ let rec explain_exn = function
           Format.printf "@\nis not convertible with@\n";
           Print.print_pure_constr a;
           Format.printf "@\n====== universes ====@\n";
-          Pp.pp (Univ.pr_universes
+          chk_pp
+            (Univ.pr_universes
             (ctx.Environ.env_stratification.Environ.env_universes));
           str "\nCantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
@@ -315,15 +307,13 @@ let rec explain_exn = function
 		   str ", characters " ++ int e ++ str "-" ++
 		   int (e+6) ++ str ")")) ++
 	       report ())
-  | e -> Errors.print e (* for anomalies and other uncaught exceptions *)
+  | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
 
 let parse_args argv =
   let rec parse = function
     | [] -> ()
     | "-impredicative-set" :: rem ->
       set_impredicative_set (); parse rem
-    | "-type-in-type" :: rem ->
-      set_type_in_type (); parse rem
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
@@ -337,15 +327,13 @@ let parse_args argv =
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
-    | "-R" :: d :: "-as" :: [] -> usage ()
     | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        Envars.set_coqlib ~fail:Errors.error;
+        Envars.set_coqlib ~fail:CErrors.error;
         print_endline (Envars.coqlib ());
         exit 0
 
@@ -383,7 +371,7 @@ let init_with_argv argv =
     try
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;
-      Envars.set_coqlib ~fail:Errors.error;
+      Envars.set_coqlib ~fail:CErrors.error;
       if_verbose print_header ();
       init_load_path ();
       engage ();