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, 61 insertions, 61 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ef3845857..0a90e0dbd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -663,7 +663,7 @@ let evar_of_binder holes = function
   try
     let h = List.nth holes (pred n) in
     h.hole_evar
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     errorlabstrm "" (str "No such binder.")
 
 let define_with_type sigma env ev c =
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index da2eee32a..04a2eb487 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -125,5 +125,5 @@ let unify ?(flags=fail_quick_unif_flags) m =
     try
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
-    with e when Errors.noncritical e -> Proofview.tclZERO e
+    with e when CErrors.noncritical e -> Proofview.tclZERO e
   end }
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 3192a6a29..58b881174 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Evd
@@ -52,7 +52,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
         (loc,"", str "Instance is not well-typed in the environment of " ++
diff --git a/proofs/logic.ml b/proofs/logic.ml
index bfaeae712..aa0b9bac6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -59,7 +59,7 @@ let is_unification_error = function
 | _ -> false
 
 let catchable_exception = function
-  | Errors.UserError _ | TypeError _
+  | CErrors.UserError _ | TypeError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index bf1da8ac0..30b031a60 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -39,7 +39,7 @@ let cook_this_proof p =
   match p with
   | { Proof_global.id;entries=[constr];persistence;universes } ->
       (id,(constr,universes,persistence))
-  | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
+  | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let cook_proof () =
   cook_this_proof (fst
@@ -59,9 +59,9 @@ let get_universe_binders () =
   Proof_global.get_universe_binders ()
 
 exception NoSuchGoal
-let _ = Errors.register_handler begin function
-  | NoSuchGoal -> Errors.error "No such goal."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoSuchGoal -> CErrors.error "No such goal."
+  | _ -> raise CErrors.Unhandled
 end
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
@@ -76,12 +76,12 @@ let get_goal_context_gen i =
 
 let get_goal_context i =
   try get_goal_context_gen i
-  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
-     | NoSuchGoal -> Errors.error "No such goal."
+  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+     | NoSuchGoal -> CErrors.error "No such goal."
 
 let get_current_goal_context () =
   try get_goal_context_gen 1
-  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
      | NoSuchGoal -> 
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
@@ -102,7 +102,7 @@ let get_current_context () =
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
     | (id,([concl],strength)) -> id,strength,concl
-    | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
+    | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
 
 let solve ?with_end_tac gi info_lvl tac pr =
   try 
@@ -127,11 +127,11 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     (p,status)
   with
-    | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
+    | Proof_global.NoCurrentProof  -> CErrors.error "No focused proof"
     | CList.IndexOutOfRange ->
         match gi with
 	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
-	                            Errors.errorlabstrm "" msg
+	                            CErrors.errorlabstrm "" msg
         | _ -> assert false
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
@@ -157,7 +157,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     delete_current_proof ();
     const, status, fst univs
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     delete_current_proof ();
     iraise reraise
 
@@ -188,7 +188,7 @@ let refine_by_tactic env sigma ty tac =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
       (** Catch the inner error of the monad tactic *)
-      let (_, info) = Errors.push src in
+      let (_, info) = CErrors.push src in
       iraise (e, info)
   in
   (** Plug back the retrieved sigma *)
@@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk =
       when
 	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
+      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
       (try
         let (ans, _, _) = 
 	  build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 86af420dc..5fe29653d 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -64,17 +64,17 @@ exception NoSuchGoals of int * int
 
 exception FullyUnfocused
 
-let _ = Errors.register_handler begin function
+let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Errors.error "This proof is focused, but cannot be unfocused this way"
+    CErrors.error "This proof is focused, but cannot be unfocused this way"
   | NoSuchGoals (i,j) when Int.equal i j ->
-      Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+      CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      Errors.errorlabstrm "Focus" Pp.(
+      CErrors.errorlabstrm "Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
-  | FullyUnfocused -> Errors.error "The proof is not focused"
-  | _ -> raise Errors.Unhandled
+  | FullyUnfocused -> CErrors.error "The proof is not focused"
+  | _ -> raise CErrors.Unhandled
 end
 
 let check_cond_kind c k =
@@ -300,12 +300,12 @@ exception UnfinishedProof
 exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
-let _ = Errors.register_handler begin function
-  | UnfinishedProof -> Errors.error "Some goals have not been solved."
-  | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
-  | HasGivenUpGoals -> Errors.error "Some goals have been given up."
-  | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | UnfinishedProof -> CErrors.error "Some goals have not been solved."
+  | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
+  | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
+  | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+  | _ -> raise CErrors.Unhandled
 end
 
 let return p =
@@ -397,9 +397,9 @@ module V82 = struct
         let evl = Evarutil.non_instantiated sigma in
         let evl = Evar.Map.bindings evl in
         if (n <= 0) then
-          Errors.error "incorrect existential variable index"
+          CErrors.error "incorrect existential variable index"
         else if CList.length evl < n then
-          Errors.error "not so many uninstantiated existential variables"
+          CErrors.error "not so many uninstantiated existential variables"
         else
           CList.nth evl (n-1)
       in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 61fe34750..7605f6387 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -34,7 +34,7 @@ let proof_modes = Hashtbl.create 6
 let find_proof_mode n =
   try Hashtbl.find proof_modes n
   with Not_found ->
-    Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
+    CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
 
 let register_proof_mode ({name = n} as m) =
   Hashtbl.add proof_modes n (CEphemeron.create m)
@@ -122,15 +122,15 @@ let push a l = l := a::!l;
   update_proof_mode ()
 
 exception NoSuchProof
-let _ = Errors.register_handler begin function
-  | NoSuchProof -> Errors.error "No such proof."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoSuchProof -> CErrors.error "No such proof."
+  | _ -> raise CErrors.Unhandled
 end
 
 exception NoCurrentProof
-let _ = Errors.register_handler begin function
-  | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+  | _ -> raise CErrors.Unhandled
 end
 
 (*** Proof Global manipulation ***)
@@ -190,7 +190,7 @@ let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    Errors.error (Pp.string_of_ppcmds
+    CErrors.error (Pp.string_of_ppcmds
       (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
        str"Use \"Abort All\" first or complete proof(s)."))
   end
@@ -202,7 +202,7 @@ let discard (loc,id) =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
-    Errors.user_err_loc
+    CErrors.user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
@@ -296,7 +296,7 @@ let set_used_variables l =
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
-        Errors.error "Used section variables can be declared only once";
+        CErrors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest;
       ctx, to_clear
 
@@ -408,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
   let evd =
     let error s =
       let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (Errors.UserError("last tactic before Qed",s ++ prf))
+      raise (CErrors.UserError("last tactic before Qed",s ++ prf))
     in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
@@ -515,12 +515,12 @@ module Bullet = struct
     exception FailedBullet of t * suggestion
 
     let _ =
-      Errors.register_handler
+      CErrors.register_handler
 	(function
 	| FailedBullet (b,sugg) ->
 	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
-	  Errors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
-	| _ -> raise Errors.Unhandled)
+	  CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
+	| _ -> raise CErrors.Unhandled)
 
 
     (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
@@ -633,7 +633,7 @@ module Bullet = struct
 	current_behavior :=
           try Hashtbl.find behaviors n
           with Not_found ->
-            Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+            CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
       end
     }
 
@@ -681,9 +681,9 @@ let parse_goal_selector = function
       let err_msg = "The default selector must be \"all\" or a natural number." in
       begin try
               let i = int_of_string i in
-              if i < 0 then Errors.error err_msg;
+              if i < 0 then CErrors.error err_msg;
               Vernacexpr.SelectNth i
-        with Failure _ -> Errors.error err_msg
+        with Failure _ -> CErrors.error err_msg
       end
 
 let _ =
@@ -712,7 +712,7 @@ type state = pstate list
 let freeze ~marshallable =
   match marshallable with
   | `Yes ->
-      Errors.anomaly (Pp.str"full marshalling of proof state not supported")
+      CErrors.anomaly (Pp.str"full marshalling of proof state not supported")
   | `Shallow -> !pstates
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index d5e3f30af..ba883b5b2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 23433692c..ebd30820b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Evd
 open Environ
@@ -240,8 +240,8 @@ let tclORELSE0 t1 t2 g =
   try
     t1 g
   with (* Breakpoint *)
-    | e when Errors.noncritical e ->
-      let e = Errors.push e in catch_failerror e; t2 g
+    | e when CErrors.noncritical e ->
+      let e = CErrors.push e in catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
@@ -253,8 +253,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in catch_failerror e; None
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
@@ -284,12 +284,12 @@ let ite_gen tcal tac_if continue tac_else gl=
       try
         tac_else gl
       with
-        e' when Errors.noncritical e' -> iraise e in
+        e' when CErrors.noncritical e' -> iraise e in
   try
     tcal tac_if0 continue gl
   with (* Breakpoint *)
-  | e when Errors.noncritical e ->
-    let e = Errors.push e in catch_failerror e; tac_else0 e gl
+  | e when CErrors.noncritical e ->
+    let e = CErrors.push e in catch_failerror e; tac_else0 e gl
 
 (* Try the first tactic and, if it succeeds, continue with
    the second one, and if it fails, use the third one *)