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

21 files changed, 114 insertions, 114 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index fb32ecac3..30b7f299f 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -15,7 +15,7 @@
    Module-traversing code: Pierre Letouzey *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3d053c2e1..180b836ea 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -10,7 +10,7 @@
    decidable equality, created by Vincent Siles, Oct 2007 *)
 
 open Tacmach
-open Errors
+open CErrors
 open Util
 open Pp
 open Term
@@ -108,7 +108,7 @@ let mkFullInd (ind,u) n =
 
 let check_bool_is_defined () =
   try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in ()
-  with e when Errors.noncritical e -> raise (UndefinedCst "bool")
+  with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
@@ -344,7 +344,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
                    (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
       (* if this happen then the args have to be already declared as a
               Parameter*)
       (
@@ -402,7 +402,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                    (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
       (* if this happen then the args have to be already declared as a
          Parameter*)
       (
@@ -423,7 +423,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         else (
           let u,v = try  destruct_ind tt1
           (* trick so that the good sequence is returned*)
-                with e when Errors.noncritical e -> indu,[||]
+                with e when CErrors.noncritical e -> indu,[||]
           in if eq_ind (fst u) ind
              then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
              else (
@@ -780,7 +780,7 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
 
 let check_not_is_defined () =
   try ignore (Coqlib.build_coq_not ())
-  with e when Errors.noncritical e -> raise (UndefinedCst "not")
+  with e when CErrors.noncritical e -> raise (UndefinedCst "not")
 
 (* {n=m}+{n<>m}  part  *)
 let compute_dec_goal ind lnamesparrec nparrec =
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index e45ab4b4e..17897460c 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Indtypes
 open Type_errors
 open Pretype_errors
@@ -36,11 +36,11 @@ let explain_exn_default = function
   | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
   (* Exceptions with pre-evaluated error messages *)
   | EvaluatedError (msg,None) -> msg
-  | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print reraise
+  | EvaluatedError (msg,Some reraise) -> msg ++ CErrors.print reraise
   (* Otherwise, not handled here *)
-  | _ -> raise Errors.Unhandled
+  | _ -> raise CErrors.Unhandled
 
-let _ = Errors.register_handler explain_exn_default
+let _ = CErrors.register_handler explain_exn_default
 
 
 (** Pre-explain a vernac interpretation error *)
@@ -112,10 +112,10 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
   let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error with_header (exc, info) in
   let () =
-    if not allow_uncaught && not (Errors.handled (fst e)) then
+    if not allow_uncaught && not (CErrors.handled (fst e)) then
       let (e, info) = e in
       let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in
-      let err = Errors.make_anomaly msg in
+      let err = CErrors.make_anomaly msg in
       Util.iraise (err, info)
   in
   let e' =
diff --git a/toplevel/class.ml b/toplevel/class.ml
index fa68a69fb..6d53ec9d8 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 235732b52..d6a6162f9 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -12,7 +12,7 @@ open Term
 open Vars
 open Environ
 open Nametab
-open Errors
+open CErrors
 open Util
 open Typeclasses_errors
 open Typeclasses
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
 	       id)
 	end
-      else Errors.error "Unsolved obligations remaining.")
+      else CErrors.error "Unsolved obligations remaining.")
 	
 let named_of_rel_context l =
   let acc, ctx =
@@ -365,7 +365,7 @@ let context poly l =
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
     try named_of_rel_context fullctx
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       error "Anonymous variables not allowed in contexts."
   in
   let uctx = ref (Evd.universe_context_set !evars) in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f3c2c43c2..f92ea027d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Flags
 open Term
@@ -964,7 +964,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
 	  | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
 	      when Reductionops.is_conv env !evdref t u -> t
 	  | _, _ -> error ()
-      with e when Errors.noncritical e -> error ()
+      with e when CErrors.noncritical e -> error ()
   in
   let measure = interp_casted_constr_evars binders_env evdref measure relargty in
   let wf_rel, wf_rel_fun, measure_fn =
@@ -1108,7 +1108,7 @@ let interp_recursive isfix fixl notations =
 	     try 
 	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
 		 Typing.e_solve_evars env evdref app
-	     with e  when Errors.noncritical e -> t
+	     with e  when CErrors.noncritical e -> t
 	   in
 	     LocalAssum (id,fixprot) :: env'
 	 else LocalAssum (id,t) :: env')
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 50a228050..5438b163a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -51,7 +51,7 @@ let load_rcfile() =
 			 " found. Skipping rcfile loading."))
 	*)
     with reraise ->
-      let reraise = Errors.push reraise in
+      let reraise = CErrors.push reraise in
       let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
   else
@@ -135,7 +135,7 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    Errors.errorlabstrm "get_compat_version"
+    CErrors.errorlabstrm "get_compat_version"
       (str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s -> Errors.errorlabstrm "get_compat_version"
+  | s -> CErrors.errorlabstrm "get_compat_version"
       (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 67a5472d5..0d4807e16 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Flags
 open Vernac
@@ -251,7 +251,7 @@ let print_toplevel_error (e, info) =
       else mt ()
     else print_location_in_file loc
   in
-  locmsg ++ Errors.iprint (e, info)
+  locmsg ++ CErrors.iprint (e, info)
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =
@@ -272,14 +272,14 @@ let rec discard_to_dot () =
   with
     | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
     | End_of_input -> raise End_of_input
-    | e when Errors.noncritical e -> ()
+    | e when CErrors.noncritical e -> ()
 
 let read_sentence () =
   try
     let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
     CWarnings.set_current_loc loc; r
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     discard_to_dot ();
     iraise reraise
 
@@ -300,13 +300,13 @@ let do_vernac () =
   try
     Vernac.eval_expr (read_sentence ())
   with
-    | End_of_input | Errors.Quit ->
-        top_stderr (fnl ()); raise Errors.Quit
-    | Errors.Drop ->  (* Last chance *)
-        if Mltop.is_ocaml_top() then raise Errors.Drop
+    | End_of_input | CErrors.Quit ->
+        top_stderr (fnl ()); raise CErrors.Quit
+    | CErrors.Drop ->  (* Last chance *)
+        if Mltop.is_ocaml_top() then raise CErrors.Drop
         else Feedback.msg_error (str"There is no ML toplevel.")
     | any ->
-        let any = Errors.push any in
+        let any = CErrors.push any in
         Format.set_formatter_out_channel stdout;
         let msg = print_toplevel_error any ++ fnl () in
         pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
@@ -343,8 +343,8 @@ let rec loop () =
     reset_input_buffer stdin top_buffer;
     while true do do_vernac(); loop_flush_all () done
   with
-    | Errors.Drop -> ()
-    | Errors.Quit -> exit 0
+    | CErrors.Drop -> ()
+    | CErrors.Quit -> exit 0
     | any ->
       Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
                 str (Printexc.to_string any) ++
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 93ed2481b..7c0b9bec2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Flags
 open Names
@@ -26,7 +26,7 @@ let get_version_date () =
     let rev = input_line ch in
     let () = close_in ch in
     (ver,rev)
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     (Coq_config.version,Coq_config.date)
 
 let print_header () =
@@ -292,7 +292,7 @@ let init_gc () =
     between coqtop and coqc. *)
 
 let usage () =
-  Envars.set_coqlib Errors.error;
+  Envars.set_coqlib CErrors.error;
   init_load_path ();
   if !batch_mode then Usage.print_usage_coqc ()
   else begin
@@ -605,8 +605,8 @@ let parse_args arglist =
   with
     | UserError(_, s) as e ->
       if is_empty s then exit 1
-      else fatal_error (Errors.print e) false
-    | any -> fatal_error (Errors.print any) (Errors.is_anomaly any)
+      else fatal_error (CErrors.print e) false
+    | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any)
 
 let init_toplevel arglist =
   init_gc ();
@@ -620,7 +620,7 @@ let init_toplevel arglist =
       (* If we have been spawned by the Spawn module, this has to be done
        * early since the master waits us to connect back *)
       Spawned.init_channels ();
-      Envars.set_coqlib Errors.error;
+      Envars.set_coqlib CErrors.error;
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
       if !print_config then (Usage.print_config (); exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
@@ -655,13 +655,13 @@ let init_toplevel arglist =
       check_vio_tasks ();
       outputstate ()
     with any ->
-      let any = Errors.push any in
+      let any = CErrors.push any in
       flush_all();
       let msg =
         if !batch_mode then mt ()
         else str "Error during initialization:" ++ fnl ()
       in
-      let is_anomaly e = Errors.is_anomaly e || not (Errors.handled e) in
+      let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in
       fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any))
   end;
   if !batch_mode then begin
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index fcb260f51..e24d5e74f 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e17cd2086..1e4c3c8f1 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -496,7 +496,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
       let fixenv = make_all_name_different fixenv in
       let pvd = pr_lconstr_env fixenv sigma vdefj.(i).uj_val in
 	str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
-    with e when Errors.noncritical e -> mt ())
+    with e when CErrors.noncritical e -> mt ())
 
 let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   let vdefj = Evarutil.jv_nf_evar sigma vdefj in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 35717ed61..6d57a21dc 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -18,7 +18,7 @@ open Libobject
 open Nameops
 open Declarations
 open Term
-open Errors
+open CErrors
 open Util
 open Declare
 open Entries
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index bbee39c3d..32e0eb53b 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -15,7 +15,7 @@
    declaring new schemes *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Declarations
@@ -157,7 +157,7 @@ let alarm what internal msg =
 let try_declare_scheme what f internal names kn =
   try f internal names kn
   with e ->
-  let e = Errors.push e in
+  let e = CErrors.push e in
   let msg = match fst e with
     | ParameterWithoutEquality cst ->
 	alarm what internal
@@ -186,9 +186,9 @@ let try_declare_scheme what f internal names kn =
     | DecidabilityMutualNotSupported ->
         alarm what internal
           (str "Decidability lemma for mutual inductive types not supported.")
-    | e when Errors.noncritical e ->
+    | e when CErrors.noncritical e ->
         alarm what internal
-	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
+	  (str "Unexpected error during scheme creation: " ++ CErrors.print e)
     | _ -> iraise e
   in
   match msg with
@@ -278,7 +278,7 @@ let try_declare_eq_decidability kn =
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
 let ignore_error f x =
-  try ignore (f x) with e when Errors.noncritical e -> ()
+  try ignore (f x) with e when CErrors.noncritical e -> ()
 
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
@@ -304,7 +304,7 @@ let declare_congr_scheme ind =
   if Hipattern.is_equality_type (mkInd ind) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
-      with e when Errors.noncritical e -> false
+      with e when CErrors.noncritical e -> false
     then
       ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
     else
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 62aa85160..154f787ef 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -18,7 +18,7 @@ let check_locality locality_flag =
   match locality_flag with
   | Some b ->
     let s = if b then "Local" else "Global" in
-    Errors.errorlabstrm "Locality.check_locality"
+    CErrors.errorlabstrm "Locality.check_locality"
       (str "This command does not support the \"" ++ str s ++ str "\" prefix.")
   | None -> ()
 
@@ -35,9 +35,9 @@ let enforce_locality_full locality_flag local =
   let local =
     match locality_flag with
     | Some false when local ->
-	Errors.error "Cannot be simultaneously Local and Global."
+	CErrors.error "Cannot be simultaneously Local and Global."
     | Some true when local ->
-	Errors.error "Use only prefix \"Local\"."
+	CErrors.error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
 	    warn_deprecated_local_syntax ();
@@ -66,7 +66,7 @@ let enforce_locality_exp locality_flag local =
   | None, Some local -> local
   | Some b, None -> local_of_bool b
   | None, None -> Decl_kinds.Global
-  | Some _, Some _ -> Errors.error "Local non allowed in this case"
+  | Some _, Some _ -> CErrors.error "Local non allowed in this case"
 
 (* For commands whose default is to not discharge but to export:
    Global in sections forces discharge, Global not in section is the default;
@@ -87,7 +87,7 @@ let enforce_section_locality locality_flag local =
 let make_module_locality = function
   | Some false ->
       if Lib.sections_are_opened () then
-	Errors.error
+	CErrors.error
 	  "This command does not support the Global option in sections.";
       false
   | Some true -> true
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index aa6601a7d..a1edb7139 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -8,7 +8,7 @@
 
 open Pp
 open Flags
-open Errors
+open CErrors
 open Util
 open Names
 open Constrexpr
@@ -184,7 +184,7 @@ let parse_format ((loc, str) : lstring) =
     else
       error "Empty format."
   with reraise ->
-    let (e, info) = Errors.push reraise in
+    let (e, info) = CErrors.push reraise in
     let info = Loc.add_loc info loc in
     iraise (e, info)
 
@@ -1057,7 +1057,7 @@ let with_lib_stk_protection f x =
   let fs = Lib.freeze `No in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let () = Lib.unfreeze fs in
     iraise reraise
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index acd8026f9..fbd1e6033 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Flags
@@ -118,8 +118,8 @@ let ml_load s =
     | WithTop t ->
       (try t.load_obj s; s
        with
-       | e when Errors.noncritical e ->
-        let e = Errors.push e in
+       | e when CErrors.noncritical e ->
+        let e = CErrors.push e in
         match fst e with
         | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
         | exc ->
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index bea96d0b7..750f7a60c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -17,7 +17,7 @@ open Vars
 open Names
 open Evd
 open Pp
-open Errors
+open CErrors
 open Util
 
 let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
@@ -258,7 +258,7 @@ let safe_init_constant md name () =
   Coqlib.gen_constant "Obligations" md name
 let hide_obligation = safe_init_constant tactics_module "obligation"
 
-let pperror cmd = Errors.errorlabstrm "Program" cmd
+let pperror cmd = CErrors.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
@@ -320,7 +320,7 @@ type program_info = program_info_aux CEphemeron.key
 let get_info x =
   try CEphemeron.get x
   with CEphemeron.InvalidKey ->
-    Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
+    CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
 
 let assumption_message = Declare.assumption_message
 
@@ -870,9 +870,9 @@ let obligation_terminator name num guard hook auto pf =
 	    if not (Int.Set.is_empty deps) then
 	    ignore (auto (Some name) None deps)
 	  end
-      with e when Errors.noncritical e ->
-        let e = Errors.push e in
-        pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
+      with e when CErrors.noncritical e ->
+        let e = CErrors.push e in
+        pperror (CErrors.iprint (Cerrors.process_vernac_interp_error e))
 
 let obligation_hook prg obl num auto ctx' _ gr =
   let obls, rem = prg.prg_obligations in
@@ -901,9 +901,9 @@ in
   let prg = { prg with prg_ctx = ctx' } in
   let () =
     try ignore (update_obls prg obls (pred rem))
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in
-      pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      pperror (CErrors.iprint (Cerrors.process_vernac_interp_error e))
   in
   if pred rem > 0 then begin
     let deps = dependencies obls num in
@@ -982,8 +982,8 @@ and solve_obligation_by_tac prg obls i tac =
 		  Some {prg with prg_ctx = ctx'})
 	      else Some prg
 	  else None
-	with e when Errors.noncritical e ->
-          let (e, _) = Errors.push e in
+	with e when CErrors.noncritical e ->
+          let (e, _) = CErrors.push e in
           match e with
 	  | Refiner.FailError (_, s) ->
 	      user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f8c70f0af..71d070776 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Globnames
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 972d83055..3423a8b8c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -9,7 +9,7 @@
 (* Parsing of vernacular. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Flags
 open Vernacexpr
@@ -67,10 +67,10 @@ let _ =
       Goptions.optwrite = ((:=) atomic_load) }
 
 let disable_drop = function
-  | Drop -> Errors.error "Drop is forbidden."
+  | Drop -> CErrors.error "Drop is forbidden."
   | e -> e
 
-let user_error loc s = Errors.user_err_loc (loc,"_",str s)
+let user_error loc s = CErrors.user_err_loc (loc,"_",str s)
 
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
@@ -91,7 +91,7 @@ let close_input in_chan (_,verb) =
     match verb with
       | Some verb_ch -> close_in verb_ch
       | _ -> ()
-  with e when Errors.noncritical e -> ()
+  with e when CErrors.noncritical e -> ()
 
 let verbose_phrase verbch loc =
   let loc = Loc.unloc loc in
@@ -196,7 +196,7 @@ let rec vernac_com verbose checknav (loc,com) =
             read_vernac_file verbosely f;
 	    restore_translator_coqdoc st;
 	  with reraise ->
-            let reraise = Errors.push reraise in
+            let reraise = CErrors.push reraise in
 	    restore_translator_coqdoc st;
 	    iraise reraise
 	end
@@ -214,7 +214,7 @@ let rec vernac_com verbose checknav (loc,com) =
       interp com;
       CLexer.restore_com_state a
     with reraise ->
-      let (reraise, info) = Errors.push reraise in
+      let (reraise, info) = CErrors.push reraise in
       Format.set_formatter_out_channel stdout;
       let loc' = Option.default Loc.ghost (Loc.get_loc info) in
       if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
@@ -235,7 +235,7 @@ and read_vernac_file verbosely s =
       vernac_com verbosely checknav loc_ast
     done
   with any ->   (* whatever the exception *)
-    let (e, info) = Errors.push any in
+    let (e, info) = CErrors.push any in
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
     match e with
@@ -262,7 +262,7 @@ let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
 let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
 
-(* Load a vernac file. Errors are annotated with file and location *)
+(* Load a vernac file. CErrors are annotated with file and location *)
 let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
@@ -270,7 +270,7 @@ let load_vernac verb file =
     Flags.silently (read_vernac_file verb) file;
     if !Flags.beautify_file then close_out !chan_beautify;
   with any ->
-    let (e, info) = Errors.push any in
+    let (e, info) = CErrors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
     iraise (disable_drop e, info)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 65aa46bc1..04c01f3cd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -9,7 +9,7 @@
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Flags
 open Names
@@ -353,7 +353,7 @@ let dump_universes_gen g s =
     close ();
     Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     close ();
     iraise reraise
 
@@ -411,7 +411,7 @@ let dump_global r =
   try
     let gr = Smartlocate.smart_global r in
     Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr
-  with e when Errors.noncritical e -> ()
+  with e when CErrors.noncritical e -> ()
 (**********)
 (* Syntax *)
 
@@ -548,9 +548,9 @@ let vernac_inductive poly lo finite indl =
       indl;
   match indl with
   | [ ( _ , _ , _ ,Record, Constructors _ ),_ ] ->
-      Errors.error "The Record keyword cannot be used to define a variant type. Use Variant instead."
+      CErrors.error "The Record keyword cannot be used to define a variant type. Use Variant instead."
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
-      Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
+      CErrors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class true -> Class false | _ -> b)
        poly finite id bl c oc fs
@@ -561,16 +561,16 @@ let vernac_inductive poly lo finite indl =
   	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) poly finite id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
-      Errors.error "Definitional classes must have a single method"
+      CErrors.error "Definitional classes must have a single method"
   | [ ( id , bl , c , Class false, Constructors _), _ ] ->
-      Errors.error "Inductive classes not supported"
+      CErrors.error "Inductive classes not supported"
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
-      Errors.error "where clause not supported for (co)inductive records"
+      CErrors.error "where clause not supported for (co)inductive records"
   | _ -> let unpack = function
       | ( (false, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
       | ( (true,_),_,_,_,Constructors _),_ ->
-          Errors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead."
-      | _ -> Errors.error "Cannot handle mutually (co)inductive records."
+          CErrors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead."
+      | _ -> CErrors.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
     do_mutual_inductive indl poly lo finite
@@ -900,7 +900,7 @@ let vernac_chdir = function
 	  (* Cd is typically used to control the output directory of
 	  extraction. A failed Cd could lead to overwriting .ml files
 	  so we make it an error. *)
-	  Errors.error ("Cd failed: " ^ err)
+	  CErrors.error ("Cd failed: " ^ err)
       end;
       if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
@@ -1654,7 +1654,7 @@ let vernac_focus gln =
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
-         Errors.error "Invalid goal number: 0. Goal numbering starts with 1."
+         CErrors.error "Invalid goal number: 0. Goal numbering starts with 1."
       | Some n ->
          Proof.focus focus_command_cond () n p)
 
@@ -1878,12 +1878,12 @@ let interp ?proof ~loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbort id -> Errors.errorlabstrm "" (str "Abort cannot be used through the Load command")
-  | VernacAbortAll -> Errors.errorlabstrm "" (str "AbortAll cannot be used through the Load command")
-  | VernacRestart -> Errors.errorlabstrm "" (str "Restart cannot be used through the Load command")
-  | VernacUndo _ -> Errors.errorlabstrm "" (str "Undo cannot be used through the Load command")
-  | VernacUndoTo _ -> Errors.errorlabstrm "" (str "UndoTo cannot be used through the Load command")
-  | VernacBacktrack _ -> Errors.errorlabstrm "" (str "Backtrack cannot be used through the Load command")
+  | VernacAbort id -> CErrors.errorlabstrm "" (str "Abort cannot be used through the Load command")
+  | VernacAbortAll -> CErrors.errorlabstrm "" (str "AbortAll cannot be used through the Load command")
+  | VernacRestart -> CErrors.errorlabstrm "" (str "Restart cannot be used through the Load command")
+  | VernacUndo _ -> CErrors.errorlabstrm "" (str "Undo cannot be used through the Load command")
+  | VernacUndoTo _ -> CErrors.errorlabstrm "" (str "UndoTo cannot be used through the Load command")
+  | VernacBacktrack _ -> CErrors.errorlabstrm "" (str "Backtrack cannot be used through the Load command")
   
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -1939,7 +1939,7 @@ let check_vernac_supports_locality c l =
     | VernacDeclareReduction _
     | VernacExtend _ 
     | VernacInductive _) -> ()
-  | Some _, _ -> Errors.error "This command does not support Locality"
+  | Some _, _ -> CErrors.error "This command does not support Locality"
 
 (* Vernaculars that take a polymorphism flag *)
 let check_vernac_supports_polymorphism c p =
@@ -1953,7 +1953,7 @@ let check_vernac_supports_polymorphism c p =
     | VernacInstance _ | VernacDeclareInstances _
     | VernacHints _ | VernacContext _
     | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
-  | Some _, _ -> Errors.error "This command does not support Polymorphism"
+  | Some _, _ -> CErrors.error "This command does not support Polymorphism"
 
 let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
@@ -2007,12 +2007,12 @@ let with_fail b f =
            with
            | HasNotFailed as e -> raise e
            | e ->
-              let e = Errors.push e in
-              raise (HasFailed (Errors.iprint
+              let e = CErrors.push e in
+              raise (HasFailed (CErrors.iprint
                 (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e))))
         ()
-    with e when Errors.noncritical e -> 
-      let (e, _) = Errors.push e in
+    with e when CErrors.noncritical e ->
+      let (e, _) = CErrors.push e in
       match e with
       | HasNotFailed ->
           errorlabstrm "Fail" (str "The command has not failed!")
@@ -2026,13 +2026,13 @@ let interp ?(verbosely=true) ?proof (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
   let rec aux ?locality ?polymorphism isprogcmd = function
     | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
-    | VernacProgram _ -> Errors.error "Program mode specified twice"
+    | VernacProgram _ -> CErrors.error "Program mode specified twice"
     | VernacLocal (b, c) when Option.is_empty locality -> 
       aux ~locality:b ?polymorphism isprogcmd c
     | VernacPolymorphic (b, c) when polymorphism = None -> 
       aux ?locality ~polymorphism:b isprogcmd c
-    | VernacPolymorphic (b, c) -> Errors.error "Polymorphism specified twice"
-    | VernacLocal _ -> Errors.error "Locality specified twice"
+    | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
+    | VernacLocal _ -> CErrors.error "Locality specified twice"
     | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
     | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
     | VernacStm _ -> assert false (* Done by Stm *)
@@ -2065,9 +2065,9 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         | reraise when
               (match reraise with
               | Timeout -> true
-              | e -> Errors.noncritical e)
+              | e -> CErrors.noncritical e)
           ->
-            let e = Errors.push reraise in
+            let e = CErrors.push reraise in
             let e = locate_if_not_already loc e in
             let () = restore_timeout () in
             Flags.program_mode := orig_program_mode;
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 0abc9e76d..d81e3d6b5 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -8,7 +8,7 @@
 
 open Util
 open Pp
-open Errors
+open CErrors
 
 type deprecation = bool
 type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
@@ -71,7 +71,7 @@ let call ?locality (opn,converted_args) =
   with
     | Drop -> raise Drop
     | reraise ->
-        let reraise = Errors.push reraise in
+        let reraise = CErrors.push reraise in
         if !Flags.debug then
 	  Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc);
         iraise reraise