errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)

 For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a

9 files changed, 53 insertions, 53 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index a7b381ad6..73a90f611 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Pp
 open Util
 
@@ -343,7 +343,7 @@ module Make(T : Task) = struct
   let with_n_workers n f =
     let q = create n in 
     try let rc = f q in destroy q; rc
-    with e -> let e = Errors.push e in destroy q; iraise e
+    with e -> let e = CErrors.push e in destroy q; iraise e
 
   let n_workers { active } = Pool.n_workers active
 
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 404e10427..fb2f0351d 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -9,7 +9,7 @@
 (* Created by Hugo Herbelin from contents related to lemma proofs in
    file command.ml, Aug 2009 *)
 
-open Errors
+open CErrors
 open Util
 open Flags
 open Pp
@@ -37,8 +37,8 @@ type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference ->
 let mk_hook hook = hook
 let call_hook fix_exn hook l c =
   try hook l c
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
     iraise (fix_exn e)
 
 (* Support for mutually proved theorems *)
@@ -210,8 +210,8 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
     definition_message id;
     Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
     iraise (fix_exn e)
 
 let default_thm_id = Id.of_string "Unnamed_thm"
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 2eae6f5e2..c5bd5f6f9 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -46,7 +46,7 @@ let control_channel = ref None
 let channels = ref None
 
 let init_channels () =
-  if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
+  if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice");
   let () = match !main_channel with
   | None -> ()
   | Some (Socket(mh,mpr,mpw)) ->
@@ -65,7 +65,7 @@ let init_channels () =
   | Some (Socket (ch, cpr, cpw)) ->
     controller ch cpr cpw
   | Some AnonPipe ->
-    Errors.anomaly (Pp.str "control channel cannot be a pipe")
+    CErrors.anomaly (Pp.str "control channel cannot be a pipe")
 
 let get_channels () =
   match !channels with
diff --git a/stm/stm.ml b/stm/stm.ml
index 928a0dd6f..9f86597dc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -16,7 +16,7 @@ let pp_to_richpp  = Richpp.richpp_of_pp
 let str_to_richpp = Richpp.richpp_of_string
 
 open Vernacexpr
-open Errors
+open CErrors
 open Pp
 open Names
 open Util
@@ -119,7 +119,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
     try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
     with e ->
-      let e = Errors.push e in
+      let e = CErrors.push e in
       iraise Hooks.(call_process_error_once e)
   end
 
@@ -149,8 +149,8 @@ let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
       match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
       | None -> raise (Invalid_argument "vernac_parse")
       | Some (loc, ast) -> indentation, strlen, loc, ast
-    with e when Errors.noncritical e ->
-      let (e, info) = Errors.push e in
+    with e when CErrors.noncritical e ->
+      let (e, info) = CErrors.push e in
       let loc = Option.default Loc.ghost (Loc.get_loc info) in
       Hooks.(call parse_error feedback_id loc (iprint (e, info)));
       iraise (e, info))
@@ -892,7 +892,7 @@ end = struct (* {{{ *)
       if Proof_global.there_are_pending_proofs () then
         VCS.goals id (Proof_global.get_open_goals ())
     with e ->
-      let (e, info) = Errors.push e in
+      let (e, info) = CErrors.push e in
       let good_id = !cur_id in
       VCS.reached id;
       let ie =
@@ -1038,7 +1038,7 @@ end = struct (* {{{ *)
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
-       Errors.errorlabstrm "undo_vernac_classifier"
+       CErrors.errorlabstrm "undo_vernac_classifier"
         (str "Cannot undo")
 
 end (* }}} *)
@@ -1072,7 +1072,7 @@ let record_pb_time proof_name loc time =
   end
  
 exception RemoteException of std_ppcmds
-let _ = Errors.register_handler (function
+let _ = CErrors.register_handler (function
   | RemoteException ppcmd -> ppcmd
   | _ -> raise Unhandled)
 
@@ -1106,7 +1106,7 @@ let proof_block_delimiters = ref []
 
 let register_proof_block_delimiter name static dynamic =
   if List.mem_assoc name !proof_block_delimiters then
-    Errors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+    CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
   proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
 
 let mk_doc_node id = function
@@ -1141,7 +1141,7 @@ let detect_proof_block id name =
           VCS.create_proof_block decl name
       end
     with Not_found ->
-      Errors.errorlabstrm "STM"
+      CErrors.errorlabstrm "STM"
         (str "Unknown proof block delimiter " ++ str name)
   )
 (****************************** THE SCHEDULER *********************************)
@@ -1326,8 +1326,8 @@ end = struct (* {{{ *)
       end;
       RespBuiltProof(proof,time)
     with
-    | e when Errors.noncritical e || e = Stack_overflow ->
-        let (e, info) = Errors.push e in
+    | e when CErrors.noncritical e || e = Stack_overflow ->
+        let (e, info) = CErrors.push e in
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)
         let e_error_at, e_safe_id = match Stateid.get info with
@@ -1466,7 +1466,7 @@ end = struct (* {{{ *)
       `OK proof
       end
     with e ->
-      let (e, info) = Errors.push e in
+      let (e, info) = CErrors.push e in
       (try match Stateid.get info with
       | None ->
           msg_error (
@@ -1706,7 +1706,7 @@ end = struct (* {{{ *)
          List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
                       Evd.(evar_context g))
        then
-         Errors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
+         CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
            "goals only"))
        else begin
         let (i, ast) = r_ast in
@@ -1719,9 +1719,9 @@ end = struct (* {{{ *)
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
               RespBuiltSubProof (t, Evd.evar_universe_context sigma)
-            else Errors.errorlabstrm "STM" (str"The solution is not ground")
+            else CErrors.errorlabstrm "STM" (str"The solution is not ground")
        end) ()
-    with e when Errors.noncritical e -> RespError (Errors.print e)
+    with e when CErrors.noncritical e -> RespError (CErrors.print e)
 
   let name_of_task { t_name } = t_name
   let name_of_request { r_name } = r_name
@@ -1773,7 +1773,7 @@ end = struct (* {{{ *)
         let gid = Goal.goal g in
         let f =
           try List.assoc gid res
-          with Not_found -> Errors.anomaly(str"Partac: wrong focus") in
+          with Not_found -> CErrors.anomaly(str"Partac: wrong focus") in
         if not (Future.is_over f) then
           (* One has failed and cancelled the others, but not this one *)
           if solve then Tacticals.New.tclZEROMSG
@@ -1842,8 +1842,8 @@ end = struct (* {{{ *)
     try
       vernac_interp r_for { r_what with verbose = true };
       feedback ~id:(State r_for) Processed
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
       let msg = pp_to_richpp (iprint e) in
       feedback ~id:(State r_for) (Message (Error, None, msg))
     
@@ -2056,7 +2056,7 @@ let known_state ?(redefine_qed=false) ~cache id =
            | _ -> assert false
         end
       with Not_found ->
-          Errors.errorlabstrm "STM"
+          CErrors.errorlabstrm "STM"
             (str "Unknown proof block delimiter " ++ str name)
   in
 
@@ -2068,8 +2068,8 @@ let known_state ?(redefine_qed=false) ~cache id =
     then f ()
     else
       try f ()
-      with e when Errors.noncritical e ->
-        let ie = Errors.push e in
+      with e when CErrors.noncritical e ->
+        let ie = CErrors.push e in
         error_absorbing_tactic id blockname ie in
   (* Absorb errors from f x *)
   let resilient_command f x =
@@ -2079,7 +2079,7 @@ let known_state ?(redefine_qed=false) ~cache id =
     then f x
     else
       try f x
-      with e when Errors.noncritical e -> () in
+      with e when CErrors.noncritical e -> () in
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
@@ -2146,8 +2146,8 @@ let known_state ?(redefine_qed=false) ~cache id =
             reach ~cache:`Shallow prev;
             reach view.next;
             (try vernac_interp id x;
-            with e when Errors.noncritical e ->
-              let (e, info) = Errors.push e in
+            with e when CErrors.noncritical e ->
+              let (e, info) = CErrors.push e in
               let info = Stateid.add info ~valid:prev id in
               iraise (e, info));
             wall_clock_last_fork := Unix.gettimeofday ()
@@ -2282,7 +2282,7 @@ let observe id =
     Reach.known_state ~cache:(interactive ()) id;
     VCS.print ()
   with e ->
-    let e = Errors.push e in
+    let e = CErrors.push e in
     VCS.print ();
     VCS.restore vcs;
     iraise e
@@ -2332,7 +2332,7 @@ let check_task name (tasks,rcbackup) i =
     let rc = Future.purify (Slaves.check_task name tasks) i in
     VCS.restore vcs;
     rc
-  with e when Errors.noncritical e -> VCS.restore vcs; false
+  with e when CErrors.noncritical e -> VCS.restore vcs; false
 let info_tasks (tasks,_) = Slaves.info_tasks tasks
 let finish_tasks name u d p (t,rcbackup as tasks) =
   RemoteCounter.restore rcbackup;
@@ -2345,7 +2345,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
     (u,a,true), p
   with e ->
-    let e = Errors.push e in
+    let e = CErrors.push e in
     msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
     exit 1
 
@@ -2377,7 +2377,7 @@ let merge_proof_branch ?valid ?id qast keep brname =
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
 let handle_failure (e, info) vcs tty =
-  if e = Errors.Drop then iraise (e, info) else
+  if e = CErrors.Drop then iraise (e, info) else
   match Stateid.get info with
   | None ->
       VCS.restore vcs;
@@ -2389,7 +2389,7 @@ let handle_failure (e, info) vcs tty =
       end;
       VCS.print ();
       anomaly(str"error with no safe_id attached:" ++ spc() ++
-        Errors.iprint_no_report (e, info))
+        CErrors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
       prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
@@ -2405,7 +2405,7 @@ let handle_failure (e, info) vcs tty =
 let snapshot_vio ldir long_f_dot_vo =
   finish ();
   if List.length (VCS.branches ()) > 1 then
-    Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
+    CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
   Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
     (Global.opaque_tables ())
 
@@ -2469,13 +2469,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           finish ();
           (try Future.purify (vernac_interp report_id ~route)
             {x with verbose = true }
-           with e when Errors.noncritical e ->
-             let e = Errors.push e in
+           with e when CErrors.noncritical e ->
+             let e = CErrors.push e in
              iraise (State.exn_on report_id e)); `Ok
       | VtQuery (false,(report_id,route)), VtNow ->
           (try vernac_interp report_id ~route x
            with e ->
-             let e = Errors.push e in
+             let e = CErrors.push e in
              iraise (State.exn_on report_id e)); `Ok
       | VtQuery (true,(report_id,_)), w ->
           assert(Stateid.equal report_id Stateid.dummy);
@@ -2611,7 +2611,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
     VCS.print ();
     rc
   with e ->
-    let e = Errors.push e in
+    let e = CErrors.push e in
     handle_failure e vcs tty
 
 let get_ast id =
@@ -2786,12 +2786,12 @@ let edit_at id =
     VCS.print ();
     rc
   with e ->
-    let (e, info) = Errors.push e in
+    let (e, info) = CErrors.push e in
     match Stateid.get info with
     | None ->
         VCS.print ();
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
-          Errors.print_no_report e)
+          CErrors.print_no_report e)
     | Some (_, id) ->
         prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
@@ -2820,7 +2820,7 @@ let interp verb (loc,e) =
        | _ -> not !Flags.coqtop_ui in
     try finish ~print_goals ()
     with e ->
-      let e = Errors.push e in
+      let e = CErrors.push e in
       handle_failure e vcs true
 
 let finish () = finish ()
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index ee121c46a..a0b08778b 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -87,7 +87,7 @@ let broadcast { lock = m; cond = c } =
   Mutex.unlock m
 
 let push { queue = q; lock = m; cond = c; release } x =
-  if release then Errors.anomaly(Pp.str
+  if release then CErrors.anomaly(Pp.str
     "TQueue.push while being destroyed! Only 1 producer/destroyer allowed");
   Mutex.lock m;
   PriorityQueue.push q x;
diff --git a/stm/vcs.ml b/stm/vcs.ml
index c483ea4a9..d3886464d 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 
 module type S = sig
 
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f6d8c327e..fa7acd00a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Vernacexpr
-open Errors
+open CErrors
 open Pp
 
 let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index d4dcf72c1..a6237daa0 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -24,7 +24,7 @@ end
 module Pool = Map.Make(IntOT)
 
 let schedule_vio_checking j fs =
-  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
@@ -98,7 +98,7 @@ let schedule_vio_checking j fs =
   exit !rc
 
 let schedule_vio_compilation j fs =
-  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index b94fae547..9623765de 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -52,7 +52,7 @@ let master_handshake worker_id ic oc =
       Printf.eprintf "Handshake with %s failed: protocol mismatch\n" worker_id;
       exit 1;
     end
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     Printf.eprintf "Handshake with %s failed: %s\n"
       worker_id (Printexc.to_string e);
     exit 1
@@ -65,7 +65,7 @@ let worker_handshake slave_ic slave_oc =
       exit 1;
     end;
     Marshal.to_channel slave_oc v []; flush slave_oc;
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     prerr_endline ("Handshake failed: " ^ Printexc.to_string e);
     exit 1