diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-27 11:03:43 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 12:08:03 +0200 |
| commit | f14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch) | |
| tree | 8a331593d0d1b518e8764c92ac54e3b11c222358 | |
| parent | 500d38d0887febb614ddcadebaef81e0c7942584 (diff) | |
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
243 files changed, 731 insertions, 731 deletions
diff --git a/Makefile.build b/Makefile.build index 7dff7f2fc..ebf2996f1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -336,7 +336,7 @@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) # coqmktop -COQMKTOPCMO:=lib/clib.cma lib/errors.cmo tools/tolink.cmo tools/coqmktop.cmo +COQMKTOPCMO:=lib/clib.cma lib/cErrors.cmo tools/tolink.cmo tools/coqmktop.cmo $(COQMKTOP): $(call bestobj, $(COQMKTOPCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -350,7 +350,7 @@ tools/tolink.ml: Makefile.build Makefile.common # coqc -COQCCMO:=lib/clib.cma lib/errors.cmo toplevel/usage.cmo tools/coqc.cmo +COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -388,7 +388,7 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) # The full coqdep (unused by this build, but distributed by make install) -COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/cWarnings.cmo lib/minisys.cmo \ +COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo lib/minisys.cmo \ lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \ tools/coqdep.cmo @@ -428,7 +428,7 @@ $(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkm # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -FAKEIDECMO:= lib/clib.cma lib/errors.cmo lib/spawn.cmo ide/document.cmo \ +FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \ ide/xmlprotocol.cmo tools/fake_ide.cmo diff --git a/Makefile.ide b/Makefile.ide index 21821bfea..48a269ab7 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -41,7 +41,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) -IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo +IDEDEPS:=lib/clib.cma lib/cErrors.cmo lib/spawn.cmo IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma diff --git a/checker/check.ml b/checker/check.ml index da3cd0316..863cf7b2c 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names diff --git a/checker/check.mllib b/checker/check.mllib index 1925477e0..488507a13 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -34,7 +34,7 @@ Feedback Segmenttree Unicodetable Unicode -Errors +CErrors CWarnings CEphemeron Future diff --git a/checker/checker.ml b/checker/checker.ml index 2c872f272..0c411ae44 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 @@ -71,7 +71,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d - with Errors.UserError _ -> + with CErrors.UserError _ -> if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -303,7 +303,7 @@ 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 @@ -329,7 +329,7 @@ let parse_args argv = | "-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 @@ -367,7 +367,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 (); diff --git a/checker/environ.ml b/checker/environ.ml index 881284eda..7b59c6b98 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -1,4 +1,4 @@ -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/include b/checker/include index f5bd2984e..6bea3c91a 100644 --- a/checker/include +++ b/checker/include @@ -31,7 +31,7 @@ open Typeops;; open Check;; open Pp;; -open Errors;; +open CErrors;; open Util;; open Names;; open Term;; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 40f55a571..27f79e796 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/inductive.ml b/checker/inductive.ml index 8bbd0f142..cb344c7fd 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/modops.ml b/checker/modops.ml index 442f999bb..b720fb621 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names diff --git a/checker/reduction.ml b/checker/reduction.ml index 97cf6ca75..ec16aa261 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Cic open Term diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index e644febe4..11cd742ba 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Cic open Names @@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - Errors.error "Needs option -impredicative-set." + CErrors.error "Needs option -impredicative-set." | _ -> () end; () diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 46d21f6cc..7eae9b831 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Names open Cic @@ -302,7 +302,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/checker/term.ml b/checker/term.ml index 56cc9cdc2..591348cb6 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -8,7 +8,7 @@ (* This module instantiates the structure of generic deBruijn terms to Coq *) -open Errors +open CErrors open Util open Names open Esubst diff --git a/checker/typeops.ml b/checker/typeops.ml index 886689329..173e19ce1 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/univ.ml b/checker/univ.ml index 96d827013..668f3a058 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -14,7 +14,7 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) open Pp -open Errors +open CErrors open Util (* Universes are stratified by a partial ordering $\le$. diff --git a/dev/printers.mllib b/dev/printers.mllib index e15855ef2..9b4998c67 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -37,7 +37,7 @@ Feedback Segmenttree Unicodetable Unicode -Errors +CErrors CWarnings Bigint CUnix diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6074acea4..7c010e6a4 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -514,7 +514,7 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (Errors.print e) + e -> Feedback.msg_notice (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; @@ -530,7 +530,7 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (Errors.print e) + e -> Feedback.msg_notice (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df1424e1c..b63391913 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term diff --git a/engine/evd.ml b/engine/evd.ml index 1276c5994..196f44760 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -999,7 +999,7 @@ let declare_principal_goal evk evd = | None -> { evd with future_goals = evk::evd.future_goals; principal_future_goal=Some evk; } - | Some _ -> Errors.error "Only one main subgoal per instantiation." + | Some _ -> CErrors.error "Only one main subgoal per instantiation." let future_goals evd = evd.future_goals diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 64be07b9c..17ff898b0 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -33,11 +33,11 @@ exception Timeout interrupts). *) exception TacticFailure of exn -let _ = Errors.register_handler begin function - | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") - | Exception e -> Errors.print e - | TacticFailure e -> Errors.print e - | _ -> Pervasives.raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | Timeout -> CErrors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") + | Exception e -> CErrors.print e + | TacticFailure e -> CErrors.print e + | _ -> Pervasives.raise CErrors.Unhandled end (** {6 Non-logical layer} *) @@ -86,11 +86,11 @@ struct let catch = fun s h -> (); fun () -> try s () with Exception e as src -> - let (src, info) = Errors.push src in + let (src, info) = CErrors.push src in h (e, info) () let read_line = fun () -> try Pervasives.read_line () with e -> - let (e, info) = Errors.push e in raise ~info e () + let (e, info) = CErrors.push e in raise ~info e () let print_char = fun c -> (); fun () -> print_char c @@ -99,8 +99,8 @@ struct let make f = (); fun () -> try f () - 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 Util.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) @@ -112,7 +112,7 @@ struct let run = fun x -> try x () with Exception e as src -> - let (src, info) = Errors.push src in + let (src, info) = CErrors.push src in Util.iraise (e, info) end diff --git a/engine/proofview.ml b/engine/proofview.ml index d87686065..905e1c079 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -309,9 +309,9 @@ let tclIFCATCH a s f = let tclONCE = Proof.once exception MoreThanOneSuccess -let _ = Errors.register_handler begin function - | MoreThanOneSuccess -> Errors.error "This tactic has more than one success." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success." + | _ -> raise CErrors.Unhandled end (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one @@ -362,12 +362,12 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f (* This uses the hook above *) -let _ = Errors.register_handler begin function +let _ = CErrors.register_handler begin function | NoSuchGoals n -> let suffix = !nosuchgoals_hook n in - Errors.errorlabstrm "" + CErrors.errorlabstrm "" (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) - | _ -> raise Errors.Unhandled + | _ -> raise CErrors.Unhandled end (** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where @@ -443,15 +443,15 @@ let tclFOCUSID id t = (** {7 Dispatching on goals} *) exception SizeMismatch of int*int -let _ = Errors.register_handler begin function +let _ = CErrors.register_handler begin function | SizeMismatch (i,_) -> let open Pp in let errmsg = str"Incorrect number of goals" ++ spc() ++ str"(expected "++int i++str(String.plural i " tactic") ++ str")." in - Errors.errorlabstrm "" errmsg - | _ -> raise Errors.Unhandled + CErrors.errorlabstrm "" errmsg + | _ -> raise CErrors.Unhandled end (** A variant of [Monad.List.iter] where we iter over the focused list @@ -844,12 +844,12 @@ let tclPROGRESS t = if not test then tclUNIT res else - tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) exception Timeout -let _ = Errors.register_handler begin function - | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") - | _ -> Pervasives.raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | _ -> Pervasives.raise CErrors.Unhandled end let tclTIMEOUT n t = @@ -983,7 +983,7 @@ let goal_extra evars gl = let catchable_exception = function | Logic_monad.Exception _ -> false - | e -> Errors.noncritical e + | e -> CErrors.noncritical e module Goal = struct @@ -1029,7 +1029,7 @@ module Goal = struct let (gl, sigma) = nf_gmake env sigma goal in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end @@ -1052,7 +1052,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end @@ -1071,7 +1071,7 @@ module Goal = struct let sigma = Sigma.to_evar_map sigma in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end @@ -1087,7 +1087,7 @@ module Goal = struct let sigma = Sigma.to_evar_map sigma in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e end end @@ -1175,7 +1175,7 @@ module V82 = struct InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> Pv.set { ps with solution = evd; comb = sgs; } with e when catchable_exception e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in tclZERO ~info e @@ -1220,7 +1220,7 @@ module V82 = struct let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = final.comb } with Logic_monad.TacticFailure e as src -> - let (_, info) = Errors.push src in + let (_, info) = CErrors.push src in iraise (e, info) let put_status = Status.put @@ -1230,7 +1230,7 @@ module V82 = struct let wrap_exceptions f = try f () with e when catchable_exception e -> - let (e, info) = Errors.push e in tclZERO ~info e + let (e, info) = CErrors.push e in tclZERO ~info e end diff --git a/engine/termops.ml b/engine/termops.ml index ac8461a3a..a047bf53c 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops diff --git a/engine/uState.ml b/engine/uState.ml index 2fb64cd6e..c35f97b2e 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index eaaa7f025..d0ab5d803 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -180,8 +180,8 @@ let declare_vernac_argument loc s pr cl = <:str_item< do { Pptactic.declare_extra_genarg_pprule $wit$ $pr_rules$ - (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) - (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } + (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer")) + (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer")) } >> ] open Pcaml diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 86e09922c..4046ef7ae 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -8,7 +8,7 @@ (************************************************************************) open Vernacexpr -open Errors +open CErrors open Util open Pp open Printer @@ -96,7 +96,7 @@ let is_undo cmd = match cmd with (** Check whether a command is forbidden by CoqIDE *) let coqide_cmd_checks (loc,ast) = - let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in + let user_error s = CErrors.user_err_loc (loc, "CoqIde", str s) in if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then @@ -300,7 +300,7 @@ let dirpath_of_string_list s = let id = try Nametab.full_name_module qid with Not_found -> - Errors.errorlabstrm "Search.interface_search" + CErrors.errorlabstrm "Search.interface_search" (str "Module " ++ str path ++ str " not found.") in id @@ -365,12 +365,12 @@ let handle_exn (e, info) = | _ -> None in let mk_msg () = let msg = read_stdout () in - let msg = str msg ++ fnl () ++ Errors.print ~info e in + let msg = str msg ++ fnl () ++ CErrors.print ~info e in Richpp.richpp_of_pp msg in match e with - | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!" - | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!" + | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!" + | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!" | e -> match Stateid.get info with | Some (valid, _) -> valid, loc_of info, mk_msg () @@ -469,7 +469,7 @@ let print_xml = fun oc xml -> Mutex.lock m; try Xml_printer.print oc xml; Mutex.unlock m - with e -> let e = Errors.push e in Mutex.unlock m; iraise e + with e -> let e = CErrors.push e in Mutex.unlock m; iraise e let slave_logger xml_oc ?loc level message = diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 79509fe02..aecb317bc 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -607,7 +607,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) with any -> - let any = Errors.push any in + let any = CErrors.push any in Fail (handler.handle_exn any) (** brain dead code, edit if protocol messages are added/removed *) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index f49ed9a5f..04429851f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -382,18 +382,18 @@ let rec prod_constr_expr c = function let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> - Errors.user_err_loc (loc, "coerce_reference_to_id", + CErrors.user_err_loc (loc, "coerce_reference_to_id", str "This expression should be a simple identifier.") let coerce_to_id = function | CRef (Ident (loc,id),_) -> (loc,id) - | a -> Errors.user_err_loc + | a -> CErrors.user_err_loc (constr_loc a,"coerce_to_id", str "This expression should be a simple identifier.") let coerce_to_name = function | CRef (Ident (loc,id),_) -> (loc,Name id) | CHole (loc,_,_,_) -> (loc,Anonymous) - | a -> Errors.user_err_loc + | a -> CErrors.user_err_loc (constr_loc a,"coerce_to_name", str "This expression should be a name.") diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 99b229251..747687189 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -8,7 +8,7 @@ (*i*) open Pp -open Errors +open CErrors open Util open Names open Nameops diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 74de6f67f..470eb8324 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -779,7 +779,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; GRef (loc, ref, None), impls, scopes, [] - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* [id] a goal variable *) GVar (loc,id), [], [], [] diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 23bcddaea..588637b76 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.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/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index b50732e4e..10cfbe58f 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -9,7 +9,7 @@ (*i*) open Names open Decl_kinds -open Errors +open CErrors open Util open Glob_term open Constrexpr diff --git a/interp/notation.ml b/interp/notation.ml index d42307040..0798d385d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Bigint @@ -208,7 +208,7 @@ let remove_delimiters scope = let sc = find_scope scope in let newsc = { sc with delimiters = None } in match sc.delimiters with - | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") + | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try @@ -1056,6 +1056,6 @@ let with_notation_protection f x = let fs = freeze false in try let a = f x in unfreeze fs; a with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = unfreeze fs in iraise reraise diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d8e022ce6..198bd2216 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -111,7 +111,7 @@ let rec eq_notation_constr t1 t2 = match t1, t2 with (* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function - | Anonymous -> Errors.error "This expression should be a simple identifier." + | Anonymous -> CErrors.error "This expression should be a simple identifier." | Name id -> id let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na diff --git a/interp/reserve.ml b/interp/reserve.ml index 7e42c1a22..388ca0805 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -8,7 +8,7 @@ (* Reserved names *) -open Errors +open CErrors open Util open Pp open Names diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 1f28ba656..478774219 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -13,7 +13,7 @@ (* *) open Pp -open Errors +open CErrors open Libnames open Globnames open Misctypes diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 7170fd14a..f96d8acc1 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.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/interp/topconstr.ml b/interp/topconstr.ml index 4109bdb7f..2b860173a 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -8,7 +8,7 @@ (*i*) open Pp -open Errors +open CErrors open Util open Names open Nameops diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 8cbc3ab44..2d1ae68f4 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -907,7 +907,7 @@ let compile fail_on_error ?universes:(universes=0) env c = Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> - let fn = if fail_on_error then Errors.errorlabstrm "compile" else + let fn = if fail_on_error then CErrors.errorlabstrm "compile" else (fun x -> Feedback.msg_warning x) in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ diff --git a/kernel/closure.ml b/kernel/closure.ml index 817012d8e..04c1bb657 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -19,7 +19,7 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) -open Errors +open CErrors open Util open Pp open Names diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 462413bd3..3f1cf9248 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = | _ -> Cpred.add c oracle.cst_trstate in { oracle with cst_opacity; cst_trstate; } - | RelKey _ -> Errors.error "set_strategy: RelKey" + | RelKey _ -> CErrors.error "set_strategy: RelKey" let fold_strategy f { var_opacity; cst_opacity; } accu = let fvar id lvl accu = f (VarKey id) lvl accu in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6dc2a617d..134599150 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -13,7 +13,7 @@ (* This module implements kernel-level discharching of local declarations over global constants and inductive types *) -open Errors +open CErrors open Util open Names open Term diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 047da682a..acd73d97d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -224,7 +224,7 @@ and val_of_constr env c = | Some v -> v | None -> assert false with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = print_string "can not compile \n" in let () = Format.print_flush () in iraise reraise diff --git a/kernel/environ.ml b/kernel/environ.ml index 7d8c3c0af..7351a87d4 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -20,7 +20,7 @@ (* This file defines the type of environments on which the type-checker works, together with simple related functions *) -open Errors +open CErrors open Util open Names open Term diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index e28d770e8..bd91c689d 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0b99c8dc2..de97268b3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 29966facb..7b2d92716 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ diff --git a/kernel/modops.ml b/kernel/modops.ml index 6fe7e382c..0f0056ed4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -264,7 +264,7 @@ let add_retroknowledge mp = |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> Environ.register env f e |_ -> - Errors.anomaly ~label:"Modops.add_retroknowledge" + CErrors.anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term") in fun lclrk env -> diff --git a/kernel/names.ml b/kernel/names.ml index 9abc9842a..9267a64d6 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -36,7 +36,7 @@ struct let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then Errors.error x else if warn then Feedback.msg_warning (str x) + if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 44cf21cff..e2f43b93e 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -5,7 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors + +open CErrors open Names open Term open Declarations diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 2f985e15a..3c0afe380 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -5,7 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors + +open CErrors open Names open Nativelib open Reduction diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index d4a67b399..1c58c7445 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -8,7 +8,7 @@ open Util open Nativevalues open Nativecode -open Errors +open CErrors open Envars (** This file provides facilities to access OCaml compiler and dynamic linker, @@ -125,7 +125,7 @@ let call_linker ?(fatal=true) prefix f upds = if not (Sys.file_exists f) then begin let msg = "Cannot find native compiler file " ^ f in - if fatal then Errors.error msg + if fatal then CErrors.error msg else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else @@ -133,7 +133,7 @@ let call_linker ?(fatal=true) prefix f upds = if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix with Dynlink.Error e as exn -> - let exn = Errors.push exn in + let exn = CErrors.push exn in let msg = "Dynlink error, " ^ Dynlink.error_message e in if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index d6fdfefa0..8093df304 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -7,7 +7,7 @@ (************************************************************************) open Term open Names -open Errors +open CErrors open Util (** This module defines the representation of values internally used by diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 0c8772d8d..130f1eb03 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -26,10 +26,10 @@ let empty_opaquetab = Int.Map.empty, DirPath.initial (* hooks *) let default_get_opaque dp _ = - Errors.error + CErrors.error ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) let default_get_univ dp _ = - Errors.error + CErrors.error ("Cannot access universe constraints of opaque proofs in library " ^ DirPath.to_string dp) @@ -45,8 +45,8 @@ let create cu = Direct ([],cu) let turn_indirect dp o (prfs,odp) = match o with | Indirect (_,_,i) -> if not (Int.Map.mem i prfs) - then Errors.anomaly (Pp.str "Indirect in a different table") - else Errors.anomaly (Pp.str "Already an indirect opaque") + then CErrors.anomaly (Pp.str "Indirect in a different table") + else CErrors.anomaly (Pp.str "Already an indirect opaque") | Direct (d,cu) -> let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in let id = Int.Map.cardinal prfs in @@ -54,21 +54,21 @@ let turn_indirect dp o (prfs,odp) = match o with let ndp = if DirPath.equal dp odp then odp else if DirPath.equal odp DirPath.initial then dp - else Errors.anomaly + else CErrors.anomaly (Pp.str "Using the same opaque table for multiple dirpaths") in Indirect ([],dp,id), (prfs, ndp) let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque") + | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque") let iter_direct_opaque f = function - | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") | Direct (d,cu) -> Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) let discharge_direct_opaque ~cook_constr ci = function - | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") | Direct (d,cu) -> Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2dc2f0c7c..67b05e526 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -15,7 +15,7 @@ (* Equal inductive types by Jacek Chrzaszcz as part of the module system, Aug 2002 *) -open Errors +open CErrors open Util open Names open Term diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fc6155930..23c0c1c31 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -190,7 +190,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - Errors.error "Needs option -impredicative-set." + CErrors.error "Needs option -impredicative-set." | _ -> () end @@ -344,10 +344,10 @@ let check_required current_libs needed = try let actual = DPMap.find id current_libs in if not(digest_match ~actual ~required) then - Errors.error + CErrors.error ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") with Not_found -> - Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".") in Array.iter check needed @@ -365,7 +365,7 @@ let safe_push_named d env = let _ = try let _ = Environ.lookup_named id env in - Errors.error ("Identifier "^Id.to_string id^" already defined.") + CErrors.error ("Identifier "^Id.to_string id^" already defined.") with Not_found -> () in Environ.push_named d env @@ -815,8 +815,8 @@ let export ?except senv dir = let senv = try join_safe_environment ?except senv with e -> - let e = Errors.push e in - Errors.errorlabstrm "export" (Errors.iprint e) + let e = CErrors.push e in + CErrors.errorlabstrm "export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -900,7 +900,7 @@ let register_inline kn senv = let open Environ in let open Pre_env in if not (evaluable_constant kn senv.env) then - Errors.error "Register inline: an evaluable constant is expected"; + CErrors.error "Register inline: an evaluable constant is expected"; let env = pre_env senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 5efc1078e..c8ceb064d 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -110,7 +110,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let u = if poly then - Errors.error ("Checking of subtyping of polymorphic" ^ + CErrors.error ("Checking of subtyping of polymorphic" ^ " inductive types not implemented") else Instance.empty in @@ -347,7 +347,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Mod_subst.force_constr lc2 in check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -364,7 +364,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 4416770fe..15f187e5c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -8,7 +8,7 @@ open Util open Pp -open Errors +open CErrors open Names open Vars diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index be84cae6d..749b5dbaf 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -12,7 +12,7 @@ (* This module provides the main entry points for type-checking basic declarations *) -open Errors +open CErrors open Util open Names open Term diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 683f6bde5..0059111c0 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 00883ddd8..e2712615b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Errors open Util open Univ @@ -132,7 +131,7 @@ let change_node g n = let rec repr g u = let a = try UMap.find u g.entries - with Not_found -> anomaly ~label:"Univ.repr" + with Not_found -> CErrors.anomaly ~label:"Univ.repr" (str"Universe " ++ Level.pr u ++ str" undefined") in match a with diff --git a/kernel/univ.ml b/kernel/univ.ml index 126f95f1f..9224ec48d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -16,7 +16,7 @@ Sozeau, Pierre-Marie Pédrot *) open Pp -open Errors +open CErrors open Util (* Universes are stratified by a partial ordering $\le$. diff --git a/kernel/vars.ml b/kernel/vars.ml index b935ab6b9..2ca749d50 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -173,7 +173,7 @@ let subst_of_rel_context_instance sign l = | LocalDef (_,c,_)::sign', args' -> aux (substl subst c :: subst) sign' args' | [], [] -> subst - | _ -> Errors.anomaly (Pp.str "Instance and signature do not match") + | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match") in aux [] (List.rev sign) l let adjust_subst_to_rel_context sign l = diff --git a/kernel/vm.ml b/kernel/vm.ml index 702987643..eb992ef89 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -232,7 +232,7 @@ let uni_lvl_val (v : values) : Univ.universe_level = | Vatom_stk (a,stk) -> str "Vatom_stk" | _ -> assert false in - Errors.anomaly + CErrors.anomaly Pp.( strbrk "Parsing virtual machine value expected universe level, got " ++ pr) @@ -282,7 +282,7 @@ let rec whd_accu a stk = | _ -> assert false end | tg -> - Errors.anomaly + CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -306,7 +306,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) else Vconstr_block(Obj.obj o) diff --git a/lib/errors.ml b/lib/cErrors.ml index 1459141d1..1459141d1 100644 --- a/lib/errors.ml +++ b/lib/cErrors.ml diff --git a/lib/errors.mli b/lib/cErrors.mli index e5dad93fd..e5dad93fd 100644 --- a/lib/errors.mli +++ b/lib/cErrors.mli diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 68442bd7c..7b8dc2b9b 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -45,7 +45,7 @@ let create ~name ~category ?(default=Enabled) pp = | Disabled -> () | AsError -> let loc = Option.default !current_loc loc in - Errors.user_err_loc (loc,"_",pp x) + CErrors.user_err_loc (loc,"_",pp x) | Enabled -> let msg = pp x ++ str " [" ++ str name ++ str "," ++ @@ -80,7 +80,7 @@ let parse_flag s = | '+' -> (AsError, String.sub s 1 (String.length s - 1)) | '-' -> (Disabled, String.sub s 1 (String.length s - 1)) | _ -> (Enabled, s) - else Errors.error "Invalid warnings flag" + else CErrors.error "Invalid warnings flag" let rec do_all_keyword = function | [] -> [] diff --git a/lib/future.ml b/lib/future.ml index 9cdc1c20e..ea0382a63 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -30,10 +30,10 @@ let customize_not_here_msg f = not_here_msg := f exception NotReady of string exception NotHere of string -let _ = Errors.register_handler (function +let _ = CErrors.register_handler (function | NotReady name -> !not_ready_msg name | NotHere name -> !not_here_msg name - | _ -> raise Errors.Unhandled) + | _ -> raise CErrors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x @@ -136,7 +136,7 @@ let rec compute ~pure ck : 'a value = let state = if pure then None else Some (!freeze ()) in c := Val (data, state); `Val data with e -> - let e = Errors.push e in + let e = CErrors.push e in let e = fix_exn e in match e with | (NotReady _, _) -> `Exn e @@ -156,9 +156,9 @@ let chain ~pure ck f = | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v) | Val (v, None) -> match !ck with - | Finished _ -> Errors.anomaly(Pp.str + | Finished _ -> CErrors.anomaly(Pp.str "Future.chain ~pure:false call on an already joined computation") - | Ongoing _ -> Errors.anomaly(Pp.strbrk( + | Ongoing _ -> CErrors.anomaly(Pp.strbrk( "Future.chain ~pure:false call on a pure computation. "^ "This can happen if the computation was initial created with "^ "Future.from_val or if it was Future.chain ~pure:true with a "^ @@ -170,7 +170,7 @@ let replace kx y = let _, _, _, x = get kx in match !x with | Exn _ -> x := Closure (fun () -> force ~pure:false y) - | _ -> Errors.anomaly + | _ -> CErrors.anomaly (Pp.str "A computation can be replaced only if is_exn holds") let purify f x = @@ -180,13 +180,13 @@ let purify f x = !unfreeze state; v with e -> - let e = Errors.push e in !unfreeze state; Exninfo.iraise e + let e = CErrors.push e in !unfreeze state; Exninfo.iraise e let transactify f x = let state = !freeze () in try f x with e -> - let e = Errors.push e in !unfreeze state; Exninfo.iraise e + let e = CErrors.push e in !unfreeze state; Exninfo.iraise e let purify_future f x = if is_over x then f x else purify f x let compute x = purify_future (compute ~pure:false) x @@ -213,7 +213,7 @@ let map2 ?greedy f x l = let xi = chain ?greedy ~pure:true x (fun x -> try List.nth x i with Failure _ | Invalid_argument _ -> - Errors.anomaly (Pp.str "Future.map2 length mismatch")) in + CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in f xi y) 0 l let print f kx = diff --git a/lib/genarg.ml b/lib/genarg.ml index 69408fb1a..05c828d5f 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -159,7 +159,7 @@ let create_arg name = match ArgT.name name with | None -> ExtraArg (ArgT.create name) | Some _ -> - Errors.anomaly (str "generic argument already declared: " ++ str name) + CErrors.anomaly (str "generic argument already declared: " ++ str name) let make0 = create_arg @@ -181,7 +181,7 @@ struct | ExtraArg s -> if GenMap.mem s !arg0_map then let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in - Errors.anomaly msg + CErrors.anomaly msg else arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map | _ -> assert false @@ -192,7 +192,7 @@ struct with Not_found -> match M.default (ExtraArg name) with | None -> - Errors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name)) + CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name)) | Some obj -> obj (** For now, the following function is quite dummy and should only be applied diff --git a/lib/lib.mllib b/lib/lib.mllib index 4b13156d6..8791f0741 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,4 +1,4 @@ -Errors +CErrors CWarnings Bigint Segmenttree diff --git a/lib/profile.ml b/lib/profile.ml index 2350cd43a..0910db3fe 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -260,7 +260,7 @@ let time_overhead_B_C () = let _dw = dummy_spent_alloc () in let _dt = get_time () in () - with e when Errors.noncritical e -> assert false + with e when CErrors.noncritical e -> assert false done; let after = get_time () in let beforeloop = get_time () in diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 6cc48c874..e7646fb79 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build = (* - in the main process there is a race condition between slave managers (that are threads) and the main thread, hence the mutex *) if Flags.async_proofs_is_worker () then - Errors.anomaly(Pp.str"Slave processes must install remote counters"); + CErrors.anomaly(Pp.str"Slave processes must install remote counters"); Mutex.lock m; let x = f () in Mutex.unlock m; build x in let mk_thsafe_remote_getter f () = @@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build = let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in let installer f = if not (Flags.async_proofs_is_worker ()) then - Errors.anomaly(Pp.str"Only slave processes can install a remote counter"); + CErrors.anomaly(Pp.str"Only slave processes can install a remote counter"); getter := mk_thsafe_remote_getter f in (fun () -> !getter ()), installer diff --git a/lib/spawn.ml b/lib/spawn.ml index 2b9c4ccac..479176973 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -43,7 +43,7 @@ module type MainLoopModel = sig end (* Common code *) -let assert_ b s = if not b then Errors.anomaly (Pp.str s) +let assert_ b s = if not b then CErrors.anomaly (Pp.str s) (* According to http://caml.inria.fr/mantis/view.php?id=5325 * you can't use the same socket for both writing and reading (may change @@ -192,7 +192,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) let live = callback cl ~read_all:(fun () -> ML.read_all gchan) in if not live then kill p; live - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> pr_err ("Async reader raised: " ^ (Printexc.to_string e)); kill p; false) gchan diff --git a/lib/system.ml b/lib/system.ml index b27918522..af9aa5c07 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -9,7 +9,6 @@ (* $Id$ *) open Pp -open Errors open Util include Minisys @@ -133,7 +132,7 @@ let find_file_in_path ?(warn=true) paths filename = let root = Filename.dirname filename in root, filename else - errorlabstrm "System.find_file_in_path" + CErrors.errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename)) else (* the name is considered to be the transcription as a relative @@ -141,7 +140,7 @@ let find_file_in_path ?(warn=true) paths filename = to be locate respecting case *) try where_in_path ~warn paths filename with Not_found -> - errorlabstrm "System.find_file_in_path" + CErrors.errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) @@ -163,8 +162,8 @@ let is_in_system_path filename = let open_trapping_failure name = try open_out_bin name - with e when Errors.noncritical e -> - errorlabstrm "System.open" (str "Can't open " ++ str name) + with e when CErrors.noncritical e -> + CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name) let warn_cannot_remove_file = CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem" @@ -172,11 +171,11 @@ let warn_cannot_remove_file = let try_remove filename = try Sys.remove filename - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> warn_cannot_remove_file filename let error_corrupted file s = - errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") + CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -249,11 +248,11 @@ let extern_state magic filename val_0 = marshal_out channel val_0; close_out channel with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = try_remove filename in iraise reraise with Sys_error s -> - errorlabstrm "System.extern_state" (str "System error: " ++ str s) + CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s) let intern_state magic filename = try @@ -262,12 +261,12 @@ let intern_state magic filename = close_in channel; v with Sys_error s -> - errorlabstrm "System.intern_state" (str "System error: " ++ str s) + CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a with Bad_magic_number {filename=fname;actual=actual;expected=expected} -> - errorlabstrm "with_magic_number_check" + CErrors.errorlabstrm "with_magic_number_check" (str"File " ++ str fname ++ strbrk" has bad magic number " ++ int actual ++ str" (expected " ++ int expected ++ str")." ++ spc () ++ diff --git a/library/declare.ml b/library/declare.ml index f809e9742..3d063225f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -9,7 +9,7 @@ (** This module is about the low-level declaration of logical objects *) open Pp -open Errors +open CErrors open Util open Names open Libnames @@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) = obj.cst_was_seff <- false; if Global.exists_objlabel (Label.of_id (basename sp)) then constant_of_kn kn - else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) + else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) end else let () = check_exists sp in let kn', exported = Global.add_constant dir id obj.cst_decl in diff --git a/library/declaremods.ml b/library/declaremods.ml index dcd63c769..b2806a1ac 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Declarations @@ -822,7 +822,7 @@ let protect_summaries f = try f fs with reraise -> (* Something wrong: undo the whole process *) - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = Summary.unfreeze_summaries fs in iraise reraise diff --git a/library/global.ml b/library/global.ml index c53611931..e748434d2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -42,7 +42,7 @@ let () = let assert_not_parsing () = if !Flags.we_are_parsing then - Errors.anomaly ( + CErrors.anomaly ( Pp.strbrk"The global environment cannot be accessed during parsing") let safe_env () = assert_not_parsing(); !global_env diff --git a/library/globnames.ml b/library/globnames.ml index bec463ecf..a78f5f13a 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Names open Term open Mod_subst diff --git a/library/goptions.ml b/library/goptions.ml index 7bead0b63..0459417fb 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -9,7 +9,7 @@ (* This module manages customization parameters at the vernacular level *) open Pp -open Errors +open CErrors open Util open Libobject open Libnames diff --git a/library/heads.ml b/library/heads.ml index 4c9b78976..02465f22f 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -70,7 +70,7 @@ let kind_of_head env t = | Const (cst,_) -> (try on_subterm k l b (constant_head cst) with Not_found -> - Errors.anomaly + CErrors.anomaly Pp.(str "constant not found in kind_of_head: " ++ str (Names.Constant.to_string cst))) | Construct _ | CoFix _ -> diff --git a/library/impargs.ml b/library/impargs.ml index 52d5c9c91..6da7e2110 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Globnames @@ -76,7 +76,7 @@ let with_implicits flags f x = implicit_args := oflags; rslt with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = implicit_args := oflags in iraise reraise diff --git a/library/kindops.ml b/library/kindops.ml index c634193da..21b1bec33 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -25,7 +25,7 @@ let string_of_theorem_kind = function let string_of_definition_kind def = let (locality, poly, kind) = def in - let error () = Errors.anomaly (Pp.str "Internal definition kind") in + let error () = CErrors.anomaly (Pp.str "Internal definition kind") in match kind with | Definition -> begin match locality with @@ -64,4 +64,4 @@ let string_of_definition_kind def = | Global -> "Global Instance" end | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - Errors.anomaly (Pp.str "Internal definition kind") + CErrors.anomaly (Pp.str "Internal definition kind") diff --git a/library/lib.ml b/library/lib.ml index 23a2d4846..8880a8b15 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Libnames open Globnames diff --git a/library/libnames.ml b/library/libnames.ml index 99ff2f2fb..dd74e192f 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names diff --git a/library/libobject.ml b/library/libobject.ml index 3e08b38b1..caa03c85b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -31,7 +31,7 @@ let default_object s = { load_function = (fun _ _ -> ()); open_function = (fun _ _ -> ()); subst_function = (fun _ -> - Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); + CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x)} @@ -97,10 +97,10 @@ let declare_object_full odecl = let declare_object odecl = try fst (declare_object_full odecl) - with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) + with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) let declare_object_full odecl = try declare_object_full odecl - with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) + with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) (* this function describes how the cache, load, open, and export functions are triggered. *) diff --git a/library/library.ml b/library/library.ml index cead90700..12090183a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names @@ -64,7 +64,7 @@ let fetch_delayed del = let () = close_in ch in if not (String.equal digest digest') then raise (Faulty f); obj - with e when Errors.noncritical e -> raise (Faulty f) + with e when CErrors.noncritical e -> raise (Faulty f) end @@ -724,7 +724,7 @@ let save_library_to ?todo dir f otab = except Int.Set.empty in let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in Array.iteri (fun i x -> - if not(is_done_or_todo i x) then Errors.errorlabstrm "library" + if not(is_done_or_todo i x) then CErrors.errorlabstrm "library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; let sd = { @@ -756,8 +756,8 @@ let save_library_to ?todo dir f otab = if not (Nativelib.compile_library dir ast fn) then error "Could not compile the library to native code." with reraise -> - let reraise = Errors.push reraise in - let () = Feedback.msg_notice (str "Removed file " ++ str f') in + let reraise = CErrors.push reraise in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise diff --git a/library/loadpath.ml b/library/loadpath.ml index 6f4d79430..e6f6716c3 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -8,7 +8,7 @@ open Pp open Util -open Errors +open CErrors open Names open Libnames diff --git a/library/nametab.ml b/library/nametab.ml index f533bc791..fa5db37ed 100644 --- a/library/nametab.ml +++ b/library/nametab.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/library/states.ml b/library/states.ml index 2e1be764a..95bd819d6 100644 --- a/library/states.ml +++ b/library/states.ml @@ -35,7 +35,7 @@ let with_state_protection f x = try let a = f x in unfreeze st; a with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in (unfreeze st; iraise reraise) let with_state_protection_on_exception = Future.transactify diff --git a/library/summary.ml b/library/summary.ml index edea7dbe5..4fef06438 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util module Dyn = Dyn.Make(struct end) @@ -105,10 +105,10 @@ let unfreeze_summaries fs = in let fold id decl state = try fold id decl state - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in Printf.eprintf "Error unfrezing summay %s\n%s\n%!" - (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e)); + (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e)); iraise e in (** We rely on the order of the frozen list, and the order of folding *) @@ -149,7 +149,7 @@ let unfreeze_summary datas = let (name, summary) = Int.Map.find id !summaries in try summary.unfreeze_function data with e -> - let e = Errors.push e in + let e = CErrors.push e in prerr_endline ("Exception unfreezing " ^ name); iraise e) datas diff --git a/library/universes.ml b/library/universes.ml index 21d960ea3..db95607f1 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -112,7 +112,7 @@ let enforce_eq_instances_univs strict x y c = let d = if strict then ULub else UEq in let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then - Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ + CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ Pp.str " instances of different lengths"); CArray.fold_right2 (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) @@ -337,7 +337,7 @@ let existing_instance ctx inst = and a2 = Instance.to_array (UContext.instance ctx) in let len1 = Array.length a1 and len2 = Array.length a2 in if not (len1 == len2) then - Errors.errorlabstrm "Universes" + CErrors.errorlabstrm "Universes" (str "Polymorphic constant expected " ++ int len2 ++ str" levels but was given " ++ int len1) else () diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index 2e0996bf5..30aeba3bb 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Errors +open CErrors open Evar_refiner open Tacmach open Tacexpr diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 8185a14d9..c6d72e03e 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -90,7 +90,7 @@ let occurrences_of = function | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) | nl -> if List.exists (fun n -> n < 0) nl then - Errors.error "Illegal negative occurrence number."; + CErrors.error "Illegal negative occurrence number."; OnlyOccurrences nl let coerce_to_int v = match Value.to_int v with diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 725f2a534..2ee9a6c98 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -19,7 +19,7 @@ open Mod_subst open Names open Tacexpr open Glob_ops -open Errors +open CErrors open Util open Evd open Termops @@ -622,7 +622,7 @@ let hResolve id c occ t = Pretyping.understand env sigma t_hole with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) in @@ -641,7 +641,7 @@ let hResolve_auto id c t = hResolve id c n t with | UserError _ as e -> raise e - | e when Errors.noncritical e -> resolve_auto (n+1) + | e when CErrors.noncritical e -> resolve_auto (n+1) in resolve_auto 1 diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index b5494a7cb..9f2c0a93e 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -36,7 +36,7 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) | Libnames.Qualid (loc,_) -> - Errors.user_err_loc (loc, "", + CErrors.user_err_loc (loc, "", str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 0b01eeef4..e0ae98ffa 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -8,7 +8,7 @@ open Names open Pp -open Errors +open CErrors open Util open Nameops open Namegen @@ -365,7 +365,7 @@ end) = struct rewrite_relation_class [| evar; mkApp (c, params) |] in let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in Some (it_mkProd_or_LetIn t rels) - with e when Errors.noncritical e -> None) + with e when CErrors.noncritical e -> None) | _ -> None @@ -446,7 +446,7 @@ let evd_convertible env evd x y = let evd = Evarconv.consider_remaining_unif_problems env evd in let () = Evarconv.check_problems_are_solved env evd in Some evd - with e when Errors.noncritical e -> None + with e when CErrors.noncritical e -> None let convertible env evd x y = Reductionops.is_conv_leq env evd x y @@ -1407,7 +1407,7 @@ module Strategies = let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in let unfolded = try Tacred.try_red_product env sigma c - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> error "fold: the term is not unfoldable !" in try @@ -1416,7 +1416,7 @@ module Strategies = state, Success { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = (sigma, snd evars) } - with e when Errors.noncritical e -> state, Fail + with e when CErrors.noncritical e -> state, Fail } @@ -1631,7 +1631,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let tactic_init_setoid () = try init_setoid (); tclIDTAC - with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded") + with e when CErrors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded") let cl_rewrite_clause_strat progress strat clause = tclTHEN (tactic_init_setoid ()) diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 6b7ae21f3..673ac832a 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Libobject @@ -429,7 +429,7 @@ let register_ltac local tacl = let kn = Lib.make_kn id in let id_pp = pr_id id in let () = if is_defined_tac kn then - Errors.user_err_loc (loc, "", + CErrors.user_err_loc (loc, "", str "There is already an Ltac named " ++ id_pp ++ str".") in let is_shadowed = @@ -437,7 +437,7 @@ let register_ltac local tacl = match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with | Tacexpr.TacArg _ -> false | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) - with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) + with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body @@ -446,7 +446,7 @@ let register_ltac local tacl = let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> - Errors.user_err_loc (loc, "", + CErrors.user_err_loc (loc, "", str "There is no Ltac named " ++ pr_reference ident ++ str ".") in UpdateTac kn, body diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index e3d5e18c9..c709ab114 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -24,7 +24,7 @@ let register_alias key tac = let interp_alias key = try KNmap.find key !alias_map - with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) + with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) let check_alias key = KNmap.mem key !alias_map @@ -55,7 +55,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = if overwrite then tac_tab := MLTacMap.remove s !tac_tab else - Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") + CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in tac_tab := MLTacMap.add s t !tac_tab @@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = let () = if Array.length tacs <= i then raise Not_found in tacs.(i) with Not_found -> - Errors.errorlabstrm "" + CErrors.errorlabstrm "" (str "The tactic " ++ pr_tacname s ++ str " is not installed.") (***************************************************************************) diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 2bbb3b309..00722ac28 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -11,7 +11,7 @@ open Pp open Genredexpr open Glob_term open Tacred -open Errors +open CErrors open Util open Names open Nameops @@ -378,13 +378,13 @@ let dump_glob_red_expr = function try Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) - with e when Errors.noncritical e -> ()) occs + with e when CErrors.noncritical e -> ()) occs | Cbv grf | Lazy grf -> List.iter (fun r -> try Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) - with e when Errors.noncritical e -> ()) grf.rConst + with e when CErrors.noncritical e -> ()) grf.rConst | _ -> () let intern_red_expr ist = function diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 9a4beed87..397cd988d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -13,7 +13,7 @@ open Genredexpr open Glob_term open Glob_ops open Tacred -open Errors +open CErrors open Util open Names open Nameops @@ -209,7 +209,7 @@ let catching_error call_trace fail (e, info) = in if List.is_empty call_trace && List.is_empty inner_trace then fail (e, info) else begin - assert (Errors.noncritical e); (* preserved invariant *) + assert (CErrors.noncritical e); (* preserved invariant *) let new_trace = inner_trace @ call_trace in let located_exc = (e, Exninfo.add info ltac_trace_info new_trace) in fail located_exc @@ -217,8 +217,8 @@ let catching_error call_trace fail (e, info) = let catch_error call_trace f x = try f x - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in catching_error call_trace iraise e let catch_error_tac call_trace tac = @@ -813,7 +813,7 @@ let interp_may_eval f ist env sigma = function try f ist env sigma c with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) @@ -827,7 +827,7 @@ let interp_constr_may_eval ist env sigma c = try interp_may_eval interp_constr ist env sigma c with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) @@ -1867,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let op = interp_typed_pattern ist env sigma op in - let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in + let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index 73d04b810..362bf3f24 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -36,10 +36,10 @@ type debug_info = (* An exception handler *) let explain_logic_error e = - Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) + CErrors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) let explain_logic_error_no_anomaly e = - Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) + CErrors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ade31c1d3..65d49cb45 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pcoq open Constrexpr diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 014b41ae9..74994c5e3 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> - Errors.user_err_loc + CErrors.user_err_loc (aloc,"Constr:mk_cofixb", Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with @@ -380,12 +380,12 @@ GEXTEND Gram [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp) - | CPatCstr (_, r, None, l2) -> Errors.user_err_loc + | CPatCstr (_, r, None, l2) -> CErrors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Nested applications not supported.") | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp) | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp) - | _ -> Errors.user_err_loc + | _ -> CErrors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Such pattern cannot have arguments.")) |"@"; r = Prim.reference; lp = LIST0 NEXT -> diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 0d72f7b93..85eb5f5cd 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -28,7 +28,7 @@ let my_int_of_string loc s = if n > 1024 * 2048 then raise Exit; n with Failure _ | Exit -> - Errors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") + CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") GEXTEND Gram GLOBAL: @@ -93,7 +93,7 @@ GEXTEND Gram ; ne_string: [ [ s = STRING -> - if s="" then Errors.user_err_loc(!@loc, "", Pp.str"Empty string."); s + if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s ] ] ; ne_lstring: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 33ca9158c..8ecc7d015 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Tacexpr open Genredexpr @@ -145,7 +145,7 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | NoBindings -> begin try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c)) - with e when Errors.noncritical e -> ElimOnConstr clbind + with e when CErrors.noncritical e -> ElimOnConstr clbind end | _ -> ElimOnConstr clbind diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7184136e8..a4bceeb67 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -8,7 +8,7 @@ open Pp open Compat -open Errors +open CErrors open Util open Names open Constrexpr diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 7d1c63ee0..ab55b3d78 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -8,7 +8,7 @@ open Pp open Compat -open Errors +open CErrors open Util open Extend open Genarg @@ -491,7 +491,7 @@ let with_grammar_rule_protection f x = let fs = freeze false in try let a = f x in unfreeze fs; a with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = unfreeze fs in iraise reraise diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index aee0bd856..6e8b2eb0f 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -212,7 +212,7 @@ module Btauto = struct let assign = List.map map_msg assign in let l = str "[" ++ (concat (str ";" ++ spc ()) assign) ++ str "]" in str "Not a tautology:" ++ spc () ++ l - with e when Errors.noncritical e -> (str "Not a tautology") + with e when CErrors.noncritical e -> (str "Not a tautology") in Tacticals.tclFAIL 0 msg gl diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 76db2f3c2..bc53b113d 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -10,7 +10,7 @@ (* Downey,Sethi and Tarjan. *) (* Plus some e-matching and constructor handling by P. Corbineau *) -open Errors +open CErrors open Util open Pp open Goptions @@ -484,7 +484,7 @@ let build_subst uf subst = Array.map (fun i -> try term uf i - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> anomaly (Pp.str "incomplete matching")) subst diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index d2bbaf6a7..f58847caf 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,7 @@ (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) -open Errors +open CErrors open Term open Ccalgo open Pp diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index de64368e2..6f6122d50 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -20,7 +20,7 @@ open Typing open Ccalgo open Ccproof open Pp -open Errors +open CErrors open Util open Proofview.Notations open Context.Rel.Declaration diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index c0ef34305..10c09c8d6 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Constrexpr diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index f9399d682..92d408901 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -9,7 +9,7 @@ open Names open Term open Evd -open Errors +open CErrors open Util let daimon_flag = ref false diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b6c34d270..5ed426c1d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Evd @@ -277,7 +277,7 @@ let prepare_goal items gls = filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref - (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered"))) + (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered"))) let register_automation_tac tac = my_automation_tac:= tac @@ -415,7 +415,7 @@ let find_subsubgoal c ctyp skip submetas gls = se.se_meta submetas se.se_meta_list} else dfs (pred n) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin enstack_subsubgoals env se stack gls; dfs n diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 73d3d1bab..6c17dcc4f 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -58,7 +58,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= let vernac_decl_proof () = let pf = Proof_global.give_me_the_proof () in if Proof.is_done pf then - Errors.error "Nothing left to prove here." + CErrors.error "Nothing left to prove here." else begin Decl_proof_instr.go_to_proof_mode () ; diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 4c71f0410..59a0bb5a2 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Decl_expr open Names diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 5d1551106..e39d17b52 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -51,9 +51,9 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> Errors.error"Admitted isn't supported in Derive." + | Admitted _ -> CErrors.error"Admitted isn't supported in Derive." | Proved (_,Some _,_) -> - Errors.error"Cannot save a proof of Derive with an explicit name." + CErrors.error"Cannot save a proof of Derive with an explicit name." | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 94981d0e1..52f22ee60 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -13,7 +13,7 @@ open Names open Libnames open Globnames open Pp -open Errors +open CErrors open Util open Table open Extraction diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 4308b4633..312c2eab3 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -684,7 +684,7 @@ and extract_cst_app env mle mlt kn u args = let l,l' = List.chop (projection_arity (ConstRef kn)) mla in if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla - with e when Errors.noncritical e -> mla + with e when CErrors.noncritical e -> mla in (* For strict languages, purely logical signatures lead to a dummy lam (except when [Kill Ktype] everywhere). So a [MLdummy] is left diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 764223621..0692c88cd 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -9,7 +9,7 @@ (*s Production of Haskell syntax. *) open Pp -open Errors +open CErrors open Util open Names open Nameops diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index bd4831130..864d90a0f 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -8,7 +8,7 @@ open Names open Globnames -open Errors +open CErrors open Util open Miniml open Table diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 3cb3810cb..1c29a9bc2 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -9,7 +9,7 @@ (*s Production of Ocaml syntax. *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -203,7 +203,7 @@ let rec pp_expr par env args = let args = List.skipn (projection_arity r) args in let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) - with e when Errors.noncritical e -> apply (pp_global Term r)) + with e when CErrors.noncritical e -> apply (pp_global Term r)) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 7b0f14dff..a6309e61f 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -9,7 +9,7 @@ (*s Production of Scheme syntax. *) open Pp -open Errors +open CErrors open Util open Names open Miniml diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 3a9ecc9ff..ff66d915f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -15,7 +15,7 @@ open Libobject open Goptions open Libnames open Globnames -open Errors +open CErrors open Util open Pp open Miniml diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 1394f4764..eebd974ea 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -8,7 +8,7 @@ open Unify open Rules -open Errors +open CErrors open Util open Term open Vars @@ -156,7 +156,7 @@ let left_instance_tac (inst,id) continue seq= (mkApp(idc,[|ot|])) rc in let evmap, _ = try Typing.type_of (pf_env gl) evmap gt - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) else diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 92b6e828e..ffb63af07 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 3e8033da0..1248b60a7 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,7 +7,7 @@ (************************************************************************) open Term -open Errors +open CErrors open Util open Formula open Unify diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index dc5dd45ab..51bd3009a 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -501,11 +501,11 @@ let rec fourier () = with NoIneq -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then Errors.error "No inequalities"; + if !lineq=[] then CErrors.error "No inequalities"; let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] - then Errors.error "fourier failed" + then CErrors.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 146749d32..13bc81019 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,5 +1,5 @@ open Printer -open Errors +open CErrors open Util open Term open Vars @@ -52,7 +52,7 @@ let rec print_debug_queue e = let _ = match e with | Some e -> - Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); @@ -74,7 +74,7 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) then print_debug_queue (Some (fst (Cerrors.process_vernac_interp_error reraise))); iraise reraise @@ -141,7 +141,7 @@ let is_trivial_eq t = eq_constr t1 t2 && eq_constr a1 a2 | _ -> false end - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false in (* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *) res @@ -167,7 +167,7 @@ let is_incompatible_eq t = (eq_constr u1 u2 && incompatible_constructor_terms t1 t2) | _ -> false - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false in if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t); res @@ -254,7 +254,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = then (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0)) else nochange "not an equality" - with e when Errors.noncritical e -> nochange "not an equality" + with e when CErrors.noncritical e -> nochange "not an equality" in if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs"; let rec compute_substitution sub t1 t2 = @@ -625,8 +625,8 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let my_orelse tac1 tac2 g = try tac1 g - with e when Errors.noncritical e -> -(* observe (str "using snd tac since : " ++ Errors.print e); *) + with e when CErrors.noncritical e -> +(* observe (str "using snd tac since : " ++ CErrors.print e); *) tac2 g let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = @@ -1025,7 +1025,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c - | _ -> Errors.anomaly (Pp.str "Not a constant") + | _ -> CErrors.anomaly (Pp.str "Not a constant") ) } | _ -> () diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5b4fb2595..18ef53276 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,5 +1,5 @@ open Printer -open Errors +open CErrors open Util open Term open Vars @@ -358,7 +358,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) save false new_princ_name entry g_kind hook - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin begin try @@ -370,7 +370,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) then Pfedit.delete_current_proof () else () else () - with e when Errors.noncritical e -> () + with e when CErrors.noncritical e -> () end; raise (Defining_principle e) end @@ -510,7 +510,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con 0 (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) (fun _ _ _ -> ()) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin begin try @@ -522,7 +522,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con then Pfedit.delete_current_proof () else () else () - with e when Errors.noncritical e -> () + with e when CErrors.noncritical e -> () end; raise (Defining_principle e) end diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 93a89330e..85897ecee 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat = let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected." + | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected." ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] @@ -199,11 +199,11 @@ let warning_error names e = match e with | Building_graph e -> let names = pr_enum Libnames.pr_reference names in - let error = if do_observe () then (spc () ++ Errors.print e) else mt () in + let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in warn_cannot_define_graph (names,error) | Defining_principle e -> let names = pr_enum Libnames.pr_reference names in - let error = if do_observe () then Errors.print e else mt () in + let error = if do_observe () then CErrors.print e else mt () in warn_cannot_define_principle (names,error) | _ -> raise e @@ -227,15 +227,15 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - Errors.error ("Cannot generate induction principle(s)") - | e when Errors.noncritical e -> + CErrors.error ("Cannot generate induction principle(s)") + | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end | _ -> assert false (* we can only have non empty list *) end - | e when Errors.noncritical e -> + | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c424fe122..52179ae50 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -7,7 +7,7 @@ open Glob_term open Glob_ops open Globnames open Indfun_common -open Errors +open CErrors open Util open Glob_termops open Misctypes @@ -921,7 +921,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) - with e when Errors.noncritical e -> raise Continue + with e when CErrors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in let _keep_eq = @@ -1223,7 +1223,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) l := param::!l ) rels_params.(0) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> () in List.rev !l @@ -1460,7 +1460,7 @@ let do_build_inductive str "while trying to define"++ spc () ++ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ - Errors.print reraise + CErrors.print reraise in observe msg; raise reraise @@ -1476,7 +1476,7 @@ let build_inductive evd funconstants funsargs returned_types rtl = do_build_inductive evd funconstants funsargs returned_types rtl; Detyping.print_universes := pu; Constrextern.print_universes := cu - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Detyping.print_universes := pu; Constrextern.print_universes := cu; raise (Building_graph e) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 291f835ee..01e5ef7fb 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,6 +1,6 @@ open Pp open Glob_term -open Errors +open CErrors open Util open Names open Decl_kinds diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2ebbb34e4..6e33af8fb 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,5 +1,5 @@ open Context.Rel.Declaration -open Errors +open CErrors open Util open Names open Term @@ -230,7 +230,7 @@ let process_vernac_interp_error e = let warn_funind_cannot_build_inversion = CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" (fun e' -> strbrk "Cannot build inversion information" ++ - if do_observe () then (fnl() ++ Errors.print e') else mt ()) + if do_observe () then (fnl() ++ CErrors.print e') else mt ()) let derive_inversion fix_names = try @@ -272,10 +272,10 @@ let derive_inversion fix_names = functional_induction fix_names_as_constant lind; - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let e' = process_vernac_interp_error e in warn_funind_cannot_build_inversion e' - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let e' = process_vernac_interp_error e in warn_funind_cannot_build_inversion e' @@ -295,12 +295,12 @@ let warning_error names e = match e with | ToShow e -> let e = process_vernac_interp_error e in - spc () ++ Errors.print e + spc () ++ CErrors.print e | _ -> if do_observe () then let e = process_vernac_interp_error e in - (spc () ++ Errors.print e) + (spc () ++ CErrors.print e) else mt () in match e with @@ -316,8 +316,8 @@ let error_error names e = let e = process_vernac_interp_error e in let e_explain e = match e with - | ToShow e -> spc () ++ Errors.print e - | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () + | ToShow e -> spc () ++ CErrors.print e + | _ -> if do_observe () then (spc () ++ CErrors.print e) else mt () in match e with | Building_graph e -> @@ -385,7 +385,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error Array.iter (add_Function is_general) funs_kn; () end - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> on_error names e let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = @@ -475,7 +475,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); derive_inversion [fname] - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* No proof done *) () in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 2449678a1..f56e92414 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -49,7 +49,7 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (Errors.UserError("", msg)) + with Not_found -> raise (CErrors.UserError("", msg)) let filter_map filter f = @@ -73,7 +73,7 @@ let chop_rlambda_n = | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> - raise (Errors.UserError("chop_rlambda_n", + raise (CErrors.UserError("chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -85,7 +85,7 @@ let chop_rprod_n = else match rt with | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (Errors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> raise (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -110,7 +110,7 @@ let const_of_id id = in try Constrintern.locate_reference princ_ref with Not_found -> - Errors.errorlabstrm "IndFun.const_of_id" + CErrors.errorlabstrm "IndFun.const_of_id" (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = @@ -344,7 +344,7 @@ let pr_info f_info = (try Printer.pr_lconstr (Global.type_of_global_unsafe (ConstRef f_info.function_constant)) - with e when Errors.noncritical e -> mt ()) ++ fnl () ++ + with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++ @@ -371,7 +371,7 @@ let in_Function : function_info -> Libobject.obj = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant") + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant") ) with Not_found -> None @@ -399,7 +399,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive") + with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive") in let finfos = { function_constant = f; @@ -476,13 +476,13 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq" - with e when Errors.noncritical e -> raise (ToShow e) + with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl" - with e when Errors.noncritical e -> raise (ToShow e) + with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1ff254f6c..ad5d077d6 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -8,7 +8,7 @@ open Tacexpr open Declarations -open Errors +open CErrors open Util open Names open Term @@ -65,16 +65,16 @@ let observe strm = let do_observe_tac s tac g = let goal = try Printer.pr_goal g - with e when Errors.noncritical e -> assert false + with e when CErrors.noncritical e -> assert false in try let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in observe (hov 0 (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); + CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; @@ -585,7 +585,7 @@ let rec reflexivity_with_destruct_cases g = observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] | _ -> Proofview.V82.of_tactic reflexivity - with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity + with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = make_eq () in let discr_inject = @@ -998,7 +998,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (Errors.UserError("",str "Not a function")) + | _ -> raise (CErrors.UserError("",str "Not a function")) in try let finfos = find_Function_infos f in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 99a165044..de4210af5 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -11,7 +11,7 @@ open Globnames open Tactics open Indfun_common -open Errors +open CErrors open Util open Constrexpr open Vernacexpr @@ -73,7 +73,7 @@ let ident_global_exist id = let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false (** [next_ident_fresh id] returns a fresh identifier (ie not linked in global env) with base [id]. *) @@ -785,10 +785,10 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let params1 = try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) - with e when Errors.noncritical e -> [] in + with e when CErrors.noncritical e -> [] in let params2 = try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) - with e when Errors.noncritical e -> [] in + with e when CErrors.noncritical e -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ceea4fa53..5562100e9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -16,7 +16,7 @@ open Names open Libnames open Globnames open Nameops -open Errors +open CErrors open Util open Tacticals open Tacmach @@ -214,7 +214,7 @@ let print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) else begin Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); @@ -238,7 +238,7 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise)); iraise reraise @@ -441,7 +441,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Lambda(n,t,b) -> @@ -449,7 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Case(ci,t,a,l) -> @@ -645,7 +645,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b; true - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false in if forbid then @@ -704,7 +704,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a; false - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> true in let a' = infos.info in @@ -1281,12 +1281,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | Some s -> s | None -> try add_suffix current_proof_name "_subproof" - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> anomaly (Pp.str "open_new_goal with an unamed theorem") in let na = next_global_ident_away name [] in if Termops.occur_existential gls_type then - Errors.error "\"abstract\" cannot handle existentials"; + CErrors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.ghost,na) in @@ -1534,10 +1534,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); false - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin if do_observe () - then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) + then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e) else anomaly (Pp.str "Cannot create equation Lemma") ; true diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 1561c811c..459c72f9f 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -331,7 +331,7 @@ let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = | Inr _ -> None | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) (* should not use rats_to_ints *) - with x when Errors.noncritical x -> + with x when CErrors.noncritical x -> if debug then (Printf.printf "raw certificate %s" (Printexc.to_string x); flush stdout) ; @@ -378,7 +378,7 @@ let linear_prover n_spec l = let linear_prover n_spec l = try linear_prover n_spec l - with x when Errors.noncritical x -> + with x when CErrors.noncritical x -> (print_string (Printexc.to_string x); None) let compute_max_nb_cstr l d = diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index e4aa1448e..b8e5e66ca 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -998,7 +998,7 @@ struct let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in (power , env) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* if the exponent is a variable *) let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) end @@ -1170,7 +1170,7 @@ struct try let (at,env) = parse_atom env t gl in (A(at,tg,t), env,Tag.next tg) - with e when Errors.noncritical e -> (X(t),env,tg) in + with e when CErrors.noncritical e -> (X(t),env,tg) in let is_prop term = let ty = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in @@ -1318,7 +1318,7 @@ let btree_of_array typ a = let btree_of_array typ a = try btree_of_array typ a - with x when Errors.noncritical x -> + with x when CErrors.noncritical x -> failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x)) let dump_varmap typ env = @@ -1387,7 +1387,7 @@ let rec parse_hyps gl parse_arith env tg hyps = try let (c,env,tg) = parse_formula gl parse_arith env tg t in ((i,c)::lhyps, env,tg) - with e when Errors.noncritical e -> (lhyps,env,tg) + with e when CErrors.noncritical e -> (lhyps,env,tg) (*(if debug then Printf.printf "parse_arith : %s\n" x);*) @@ -1547,7 +1547,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = (pp_ml_list prover.pp_f) (List.map fst new_cl) ; flush stdout end ; *) - let res = try prover.compact prf remap with x when Errors.noncritical x -> + let res = try prover.compact prf remap with x when CErrors.noncritical x -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) match prover.prover (prover.get_option () ,List.map fst new_cl) with diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index e22fe5843..f4f9b3c2f 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -734,7 +734,7 @@ struct | Inl (s,_) -> try Some (bound_of_variable IMap.empty fresh s.sys) - with x when Errors.noncritical x -> + with x when CErrors.noncritical x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x); None diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 88b13abf9..0e6d346a3 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -92,7 +92,7 @@ let read_key_elem inch = Some (Marshal.from_channel inch) with | End_of_file -> None - | e when Errors.noncritical e -> raise InvalidTableFormat + | e when CErrors.noncritical e -> raise InvalidTableFormat (** We used to only lock/unlock regions. diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index ee1904a66..93dad18d9 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Term open Tactics diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index 8e2fc07c0..922432460 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -51,7 +51,7 @@ let facteurs_liste div constant lp = if not (constant r) then l1:=r::(!l1) else p_dans_lmin:=true) - with e when Errors.noncritical e -> ()) + with e when CErrors.noncritical e -> ()) lmin; if !p_dans_lmin then factor lmin lp1 @@ -62,7 +62,7 @@ let facteurs_liste div constant lp = List.iter (fun q -> try (let r = div q p in if not (constant r) then l1:=r::(!l1)) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> lmin1:=q::(!lmin1)) lmin; factor (List.rev (p::(!lmin1))) !l1) @@ -93,7 +93,7 @@ let factorise_tableau div zero c f l1 = li:=j::(!li); r:=rr; done) - with e when Errors.noncritical e -> ()) + with e when CErrors.noncritical e -> ()) l1; res.(i)<-(!r,!li)) f; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 0bf30e7fd..d625e3076 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -open Errors +open CErrors open Util open Names open Nameops @@ -911,7 +911,7 @@ let rec transform p t = try let v,th,_ = find_constr t' in [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let v = new_identifier_var () and th = new_identifier () in hide_constr t' v th isnat; @@ -951,7 +951,7 @@ let rec transform p t = end | Kapp((Zpos|Zneg|Z0),_) -> (try ([],Oz(recognize_number t)) - with e when Errors.noncritical e -> default false t) + with e when CErrors.noncritical e -> default false t) | Kvar s -> [],Oatom s | Kapp(Zopp,[t]) -> let tac,t' = transform (P_APP 1 :: p) t in diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index d7538146f..5647fbf9f 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -34,7 +34,7 @@ let omega_tactic l = | "positive" -> eval_tactic "zify_positive" | "N" -> eval_tactic "zify_N" | "Z" -> eval_tactic "zify_op" - | s -> Errors.error ("No Omega knowledge base for type "^s)) + | s -> CErrors.error ("No Omega knowledge base for type "^s)) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index dbd7460e2..b3ea4335f 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -101,7 +101,7 @@ (*i*) -open Errors +open CErrors open Util open Names open Term diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 21b0f78b5..4935fe4bb 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -39,7 +39,7 @@ let destructurate t = | Term.Var id,[] -> Kvar(Names.Id.to_string id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> - Errors.error "Omega: Not a quantifier-free goal" + CErrors.error "Omega: Not a quantifier-free goal" | _ -> Kufo exception Destruct @@ -346,7 +346,7 @@ let parse_term t = | Kapp("Z.succ",[t]) -> Tsucc t | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (try Tnum (recognize t) with e when Errors.noncritical e -> Tother) + (try Tnum (recognize t) with e when CErrors.noncritical e -> Tother) | _ -> Tother with e when Logic.catchable_exception e -> Tother @@ -368,6 +368,6 @@ let is_scalar t = | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true | _ -> false in - try aux t with e when Errors.noncritical e -> false + try aux t with e when CErrors.noncritical e -> false end diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index fd4ede6c3..830dc54dd 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -27,7 +27,7 @@ let romega_tactic l = | "positive" -> eval_tactic "zify_positive" | "N" -> eval_tactic "zify_N" | "Z" -> eval_tactic "zify_op" - | s -> Errors.error ("No ROmega knowledge base for type "^s)) + | s -> CErrors.error ("No ROmega knowledge base for type "^s)) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index a059512d8..ba882e39a 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -454,7 +454,7 @@ let rec scalar n = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x)) | Omult(t1,t2) -> - Errors.error "Omega: Can't solve a goal with non-linear products" + CErrors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [], Omult(t,Oint n) | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i) | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n)) @@ -473,7 +473,7 @@ let rec negate = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x)) | Omult(t1,t2) -> - Errors.error "Omega: Can't solve a goal with non-linear products" + CErrors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone)) | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i) @@ -545,7 +545,7 @@ let shrink_pair f1 f2 = Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2)) | t1,t2 -> oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); - flush Pervasives.stdout; Errors.error "shrink.1" + flush Pervasives.stdout; CErrors.error "shrink.1" end (* \subsection{Calcul d'une sous formule constante} *) @@ -559,9 +559,9 @@ let reduce_factor = function let rec compute = function Oint n -> n | Oplus(t1,t2) -> compute t1 + compute t2 - | _ -> Errors.error "condense.1" in + | _ -> CErrors.error "condense.1" in [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) - | t -> Errors.error "reduce_factor.1" + | t -> CErrors.error "reduce_factor.1" (* \subsection{Réordonnancement} *) @@ -1304,7 +1304,7 @@ let total_reflexive_omega_tactic gl = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution env full_reified_goal systems_list gl - with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system" + with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index f3eae5f50..8b9261113 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Goptions diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index bb9266db1..7367a47ea 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -8,7 +8,7 @@ module Search = Explore.Make(Proof_search) -open Errors +open CErrors open Util open Term open Tacmach diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a6744916a..c08813f6e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 814e3a4d5..ff1db8cf5 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -61,8 +61,8 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = Errors.errorlabstrm "ssrmatching" -let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg) +let errorstrm = CErrors.errorlabstrm "ssrmatching" +let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -89,7 +89,7 @@ let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] let get_index = function ArgArg i -> i | _ -> - Errors.anomaly (str"Uninterpreted index") + CErrors.anomaly (str"Uninterpreted index") (* Toplevel constr must be globalized twice ! *) let glob_constr ist genv = function | _, Some ce -> @@ -150,7 +150,7 @@ let dC t = CastConv t (** Constructors for constr_expr *) let isCVar = function CRef (Ident _, _) -> true | _ -> false let destCVar = function CRef (Ident (_, id), _) -> id | _ -> - Errors.anomaly (str"not a CRef") + CErrors.anomaly (str"not a CRef") let mkCHole loc = CHole (loc, None, IntroAnonymous, None) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) @@ -167,8 +167,8 @@ let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t) let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2)) - | _, (_, (_, None)) -> Errors.anomaly (str"have: mixed C-G constr") - | _ -> Errors.anomaly (str"have: mixed G-C constr") + | _, (_, (_, None)) -> CErrors.anomaly (str"have: mixed C-G constr") + | _ -> CErrors.anomaly (str"have: mixed G-C constr") let loc_ofCG = function | (_, (s, None)) -> Glob_ops.loc_of_glob_constr s | (_, (_, Some s)) -> Constrexpr_ops.constr_loc s @@ -491,7 +491,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = | Evar (k, _) -> if Evd.mem sigma0 k then KpatEvar k, f, a else if a <> [] then KpatFlex, f, a else - (match p_origin with None -> Errors.error "indeterminate pattern" + (match p_origin with None -> CErrors.error "indeterminate pattern" | Some (dir, rule) -> errorstrm (str "indeterminate " ++ pr_dir_side dir ++ str " in " ++ pr_constr_pat rule)) @@ -632,12 +632,12 @@ let match_upats_FO upats env sigma0 ise orig_c = let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in raise (FoundUnif (ungen_upat lhs pt' u)) with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u - | Not_found -> Errors.anomaly (str"incomplete ise in match_upats_FO") + | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO") | _ -> () in List.iter one_match fpats done; iter_constr_LR loop f; Array.iter loop a in - try loop orig_c with Invalid_argument _ -> Errors.anomaly (str"IN FO") + try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO") let prof_FO = mk_profiler "match_upats_FO";; let match_upats_FO upats env sigma0 ise c = @@ -684,7 +684,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsatisfiableConstraints _) -> failed_because_of_TC:=true - | e when Errors.noncritical e -> () in + | e when CErrors.noncritical e -> () in List.iter one_match fpats done; iter_constr_LR (aux upats env sigma0 ise) f; @@ -707,11 +707,11 @@ let fixed_upat = function let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) let assert_done r = - match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called") + match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called") let assert_done_multires r = match !r with - | None -> Errors.anomaly (str"do_once never called") + | None -> CErrors.anomaly (str"do_once never called") | Some (n, xs) -> r := Some (n+1,xs); try List.nth xs n with Failure _ -> raise NoMatch @@ -768,7 +768,7 @@ let source () = match upats_origin, upats with | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ pr_constr_pat rule ++ spc() | _, [] | None, _::_::_ -> - Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in let on_instance, instances = let instances = ref [] in (fun x -> @@ -806,7 +806,7 @@ let rec uniquize = function errorstrm (source () ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> let dir = match upats_origin with Some (d,_) -> d | _ -> - Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in errorstrm (str"all matches of "++source()++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); @@ -841,7 +841,7 @@ let rec uniquize = function let sigma, uc, ({up_f = pf; up_a = pa} as u) = match !upat_that_matched with | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch - | None -> Errors.anomaly (str"companion function never called") in + | None -> CErrors.anomaly (str"companion function never called") in let p' = mkApp (pf, pa) in if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++ @@ -1022,7 +1022,7 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) when isCVar t1 -> encode k "In" [r1; r2; bind_in t1 t2] | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] - | _ -> Errors.anomaly (str"where are we?") + | _ -> CErrors.anomaly (str"where are we?") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] @@ -1109,9 +1109,9 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let v = Id.Map.find id ist.lfun in Option.get reccall (Value.cast (topwit (Option.get wit_ssrpatternarg)) v) - | it -> g t with e when Errors.noncritical e -> g t in + | it -> g t with e when CErrors.noncritical e -> g t in let decodeG t f g = decode ist (mkG t) f g in - let bad_enc id _ = Errors.anomaly (str"bad encoding for pattern "++str id) in + let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id) in let cleanup_XinE h x rp sigma = let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) @@ -1297,7 +1297,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = let e = match p with - | In_T _ | In_X_In_T _ -> Errors.anomaly (str"pattern without redex") + | In_T _ | In_X_In_T _ -> CErrors.anomaly (str"pattern without redex") | T e | X_In_T (e, _) | E_As_X_In_T (e, _, _) | E_In_X_In_T (e, _, _) -> e in let sigma = if not resolve_typeclasses then sigma @@ -1335,7 +1335,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let fill_occ_term env cl occ sigma0 (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in - if sigma' != sigma0 then Errors.error "matching impacts evars" + if sigma' != sigma0 then CErrors.error "matching impacts evars" else cl, (Evd.merge_universe_context sigma' uc, t') with NoMatch -> try let sigma', uc, t' = diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 03b49e333..e18d19ced 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -11,7 +11,7 @@ let __coq_plugin_name = "ascii_syntax_plugin" let () = Mltop.add_known_module __coq_plugin_name open Pp -open Errors +open CErrors open Util open Names open Glob_term diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 89305838b..a9eb126b4 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -17,7 +17,7 @@ open Glob_term open Bigint open Coqlib open Pp -open Errors +open CErrors (*i*) (**********************************************************************) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 57cb2f897..f65f9b791 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n = GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") + CErrors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n = GApp (dloc, ref_constructor, args) let bigN_error_negative dloc = - Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") + CErrors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index ce86c0a65..60803a369 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Bigint diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c39a57012..985ad4b0d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 5fb6c130e..4f265e76c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Flags diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 704559dd7..913e80f39 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -14,7 +14,7 @@ Corbineau, Feb 2008 *) (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *) -open Errors +open CErrors open Util open Names open Term @@ -370,7 +370,7 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion") + | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index c566839e8..886a98263 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -8,7 +8,7 @@ (*i*) open Pp -open Errors +open CErrors open Util open Names open Globnames diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index cc178eb97..d4066f387 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -323,7 +323,7 @@ let is_nondep_branch c l = (* FIXME: do better using tags from l *) let sign,ccl = decompose_lam_n_decls (List.length l) c in noccur_between 1 (Context.Rel.length sign) ccl - with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) + with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *) false let extract_nondep_branches test c b l = @@ -631,7 +631,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c)) mat - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Array.to_list (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 729006dbb..8abe6116b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term @@ -766,7 +766,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in Success evd' with Univ.UniverseInconsistency p -> UnifFailure (evd,UnifUnivInconsistency p) - | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead)) + | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead)) | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 77b0c67ad..62700aef3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Errors +open CErrors open Names open Term open Vars @@ -1460,7 +1460,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in t::l - with e when Errors.noncritical e -> l in + with e when CErrors.noncritical e -> l in (match candidates with | [x] -> x | _ -> diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index df1fc20f1..4caa1e992 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -8,7 +8,7 @@ open Pp open Util -open Errors +open CErrors open Names open Locus open Term diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 866b2b495..0c80bd019 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -11,7 +11,7 @@ (* This file builds various inductive schemes *) open Pp -open Errors +open CErrors open Util open Names open Libnames diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 6be6a2d3a..fbad0d949 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index d89aeccd8..e4fbf8d54 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -50,9 +50,9 @@ let is_nowhere = function let simple_clause_of enum_hyps cl = let error_occurrences () = - Errors.error "This tactic does not support occurrences selection" in + CErrors.error "This tactic does not support occurrences selection" in let error_body_selection () = - Errors.error "This tactic does not support body selection" in + CErrors.error "This tactic does not support body selection" in let hyps = match cl.onhyps with | None -> @@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable") + | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable") | Misctypes.ArgArg x -> x let occurrences_of_hyp id cls = diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index e537a3c0a..0dd64697c 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Term open Vars open Environ @@ -178,7 +178,7 @@ let rec nf_val env v typ = let name,dom,codom = try decompose_prod env typ with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let env = push_rel (LocalAssum (name,dom)) env in @@ -224,7 +224,7 @@ and nf_args env accu t = let _,dom,codom = try decompose_prod env t with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env arg dom in @@ -241,7 +241,7 @@ and nf_bargs env b t = let _,dom,codom = try decompose_prod env !t with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env (block_field b i) dom in @@ -352,7 +352,7 @@ and nf_predicate env ind mip params v pT = let name,dom,codom = try decompose_prod env pT with DestKO -> - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let dep,body = diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 7eb3d633d..fe73b6105 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Globnames diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index b0715af73..00b6100c0 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -60,7 +60,7 @@ type pretype_error = exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function - | Errors.UserError _ | TypeError _ | PretypeError _ + | CErrors.UserError _ | TypeError _ | PretypeError _ | Nametab.GlobalizationError _ -> true | _ -> false diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 38defe951..c8f61c66b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -22,7 +22,7 @@ open Pp -open Errors +open CErrors open Util open Names open Evd @@ -81,7 +81,7 @@ let search_guard loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix 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)); indexes @@ -228,8 +228,8 @@ let apply_heuristics env evdref fail_evar = (* Resolve eagerly, potentially making wrong choices *) try evdref := consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env !evdref - with e when Errors.noncritical e -> - let e = Errors.push e in if fail_evar then iraise e + with e when CErrors.noncritical e -> + let e = CErrors.push e in if fail_evar then iraise e let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) @@ -624,7 +624,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix 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)); make_judge (mkCoFix cofix) ftys.(i) @@ -757,7 +757,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ try judge_of_product env name j j' with TypeError _ as e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in let info = Loc.add_loc info loc in iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon diff --git a/pretyping/program.ml b/pretyping/program.ml index 253d85742..b4333847b 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 95c6725f3..682a88333 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -13,7 +13,7 @@ (* This file registers properties of records: projections and canonical structures *) -open Errors +open CErrors open Util open Pp open Names @@ -176,7 +176,7 @@ let cs_pattern_of_constr t = App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs - with e when Errors.noncritical e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found end | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b] @@ -184,7 +184,7 @@ let cs_pattern_of_constr t = | _ -> begin try Const_cs (global_of_constr t) , None, [] - with e when Errors.noncritical e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found end let warn_projection_no_head_constant = diff --git a/pretyping/redops.ml b/pretyping/redops.ml index db5879174..7d65925e5 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -20,12 +20,12 @@ let make_red_flag l = | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then - Errors.error + CErrors.error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then - Errors.error + CErrors.error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = union_consts red.rConst l; rDelta = true } diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 29b448caa..76c4304c4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Term @@ -1206,7 +1206,7 @@ let pb_equal = function let report_anomaly _ = let e = UserError ("", Pp.str "Conversion test raised an anomaly") in - let e = Errors.push e in + let e = CErrors.push e in iraise e let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5de540a00..98b36fb92 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Term open Vars diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 51a89966f..2d07bf4d5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d57eef2e1..2c675b9ea 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -150,7 +150,7 @@ let dest_class_arity env c = let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) - with e when Errors.noncritical e -> None + with e when CErrors.noncritical e -> None let is_class_constr c = try let gr, u = Universes.global_of_constr c in @@ -249,7 +249,7 @@ let rebuild_class cl = try let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in set_typeclass_transparency cst false false; cl - with e when Errors.noncritical e -> cl + with e when CErrors.noncritical e -> cl let class_input : typeclass -> obj = declare_object @@ -272,7 +272,7 @@ let check_instance env sigma c = let (evd, c) = resolve_one_typeclass env sigma (Retyping.get_type_of env sigma c) in not (Evd.has_undefined evd) - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false let build_subclasses ~check env sigma glob pri = let _id = Nametab.basename_of_global glob in @@ -422,7 +422,7 @@ let add_class cl = match inst with | Some (Backward, pri) -> (match body with - | None -> Errors.error "Non-definable projection can not be declared as a subinstance" + | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" | Some b -> declare_instance pri false (ConstRef b)) | _ -> ()) cl.cl_projs diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 8e44fb008..0e4885bea 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Term open Vars diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5bb853b69..c17879739 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Util open Names @@ -742,7 +742,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb then Evd.set_leq_sort curenv sigma s1 s2 else Evd.set_eq_sort curenv sigma s1 s2 in (sigma', metasubst, evarsubst) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> error_cannot_unify curenv sigma (m,n)) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> @@ -1138,11 +1138,11 @@ let merge_instances env sigma flags st1 st2 c1 c2 = else (right, st2, res) | (IsSuperType,IsSubType) -> (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2)) | (IsSubType,IsSuperType) -> (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1)) (* Unification @@ -1353,7 +1353,7 @@ let w_merge env with_types flags (evd,metas,evars) = let rec process_eqns failures = function | (mv,status,c)::eqns -> (match (try Inl (unify_type env evd flags mv status c) - with e when Errors.noncritical e -> Inr e) + with e when CErrors.noncritical e -> Inr e) with | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns | Inl (evd,metas,evars) -> @@ -1555,7 +1555,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) (** MS: This is pretty bad, it catches Not_found for example *) - | e when Errors.noncritical e -> raise (NotUnifiable None) in + | e when CErrors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 0b102f921..c396f593b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -305,7 +305,7 @@ and nf_fun env f typ = try decompose_prod env typ with DestKO -> (* 27/2/13: Turned this into an anomaly *) - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let body = nf_val (push_rel (LocalAssum (name,dom)) env) vb codom in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1ea502539..252b0967d 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 0ab1349ec..917a277c9 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -9,7 +9,7 @@ open Pp open Names open Namegen -open Errors +open CErrors open Util open Constrexpr open Tacexpr diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5b73b054d..0d47b34df 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -9,7 +9,7 @@ open Pp open Names -open Errors +open CErrors open Util open Extend open Vernacexpr @@ -1082,7 +1082,7 @@ module Make ) | VernacSetOpacity _ -> return ( - Errors.anomaly (keyword "VernacSetOpacity used to set something else") + CErrors.anomaly (keyword "VernacSetOpacity used to set something else") ) | VernacSetStrategy l -> let pr_lev = function @@ -1219,7 +1219,7 @@ module Make let pr_vernac v = try pr_vernac_body v ++ sep_end v - with e -> Errors.print e + with e -> CErrors.print e end diff --git a/printing/prettyp.ml b/printing/prettyp.ml index ad67becd0..1f6e99c7e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -11,7 +11,7 @@ *) open Pp -open Errors +open CErrors open Util open Names open Nameops diff --git a/printing/printer.ml b/printing/printer.ml index 0bac2755b..28fd92659 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -184,7 +184,7 @@ let safe_gen f env sigma c = let orig_extern_ref = Constrextern.get_extern_reference () in let extern_ref loc vars r = try orig_extern_ref loc vars r - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Libnames.Qualid (loc, qualid_of_global env r) in Constrextern.set_extern_reference extern_ref; @@ -192,7 +192,7 @@ let safe_gen f env sigma c = let p = f env sigma c in Constrextern.set_extern_reference orig_extern_ref; p - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Constrextern.set_extern_reference orig_extern_ref; str "??" @@ -802,13 +802,13 @@ let pr_assumptionset env s = in let safe_pr_ltype typ = try str " : " ++ pr_ltype typ - with e when Errors.noncritical e -> mt () + with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = let sigma, env = get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ - with e when Errors.noncritical e -> mt () + with e when CErrors.noncritical e -> mt () in let pr_axiom env ax typ = match ax with diff --git a/printing/printmod.ml b/printing/printmod.ml index 5f98eeeab..c939f54e8 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -254,7 +254,7 @@ let nametab_register_modparam mbid mtb = via a Declaremods function that converts back to module entries *) try Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) let mp = MPbound mbid in let dir = DirPath.make [MBId.to_id mbid] in @@ -295,7 +295,7 @@ let print_body is_impl env mp (l,body) = try let env = Option.get env in pr_mutual_inductive_body env (MutInd.make2 mp l) mib - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let keyword = let open Decl_kinds in match mib.mind_finite with @@ -422,7 +422,7 @@ let print_module with_body mp = try if !short then raise ShortPrinting; unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl () - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> unsafe_print_module None mp with_body me ++ fnl () let print_modtype kn = @@ -433,7 +433,7 @@ let print_modtype kn = (try if !short then raise ShortPrinting; print_signature' true (Some (Global.env ())) kn mtb.mod_type - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> print_signature' true None kn mtb.mod_type)) end 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 *) 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 diff --git a/tactics/auto.ml b/tactics/auto.ml index 6c1f38d48..962af4b5c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,7 +10,7 @@ *) open Pp open Util -open Errors +open CErrors open Names open Vars open Termops @@ -222,7 +222,7 @@ let tclLOG (dbg,depth,trace) pp tac = Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); out with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); iraise reraise end @@ -234,7 +234,7 @@ let tclLOG (dbg,depth,trace) pp tac = trace := (depth, Some pp) :: !trace; out with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in trace := (depth, None) :: !trace; iraise reraise end diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 9ae0ab90b..475005648 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -13,7 +13,7 @@ open Tacticals open Tactics open Term open Termops -open Errors +open CErrors open Util open Mod_subst open Locus diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 63b5e2a70..6e01a676a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -13,7 +13,7 @@ *) open Pp -open Errors +open CErrors open Util open Names open Term @@ -382,7 +382,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = if cl.cl_strict then Evd.evars_of_term concl else Evar.Set.empty - with e when Errors.noncritical e -> Evar.Set.empty + with e when CErrors.noncritical e -> Evar.Set.empty in let hintl = List.map_append @@ -485,7 +485,7 @@ let is_unique env concl = try let (cl,u), args = dest_class_app env concl in cl.cl_unique - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false (** Sort the undefined variables from the least-dependent to most dependent. *) let top_sort evm undefs = @@ -1288,7 +1288,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) ~depth dbs = let dbs = List.map_filter (fun db -> try Some (searchtable_map db) - with e when Errors.noncritical e -> None) + with e when CErrors.noncritical e -> None) dbs in let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in @@ -1444,7 +1444,7 @@ let resolve_typeclass_evars debug depth unique env evd filter split fail = let evd = try Evarconv.consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env evd - with e when Errors.noncritical e -> evd + with e when CErrors.noncritical e -> evd in resolve_all_evars debug depth unique env (initial_select_evars filter) evd split fail diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 93c201bf1..2eca1e597 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -231,8 +231,8 @@ module SearchProblem = struct (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls, cost, pptac) :: aux tacl - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in Refiner.catch_failerror e; aux tacl in aux l diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index a03489c80..1a45217a4 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -44,7 +44,7 @@ natural expectation of the user. *) -open Errors +open CErrors open Util open Names open Term diff --git a/tactics/equality.ml b/tactics/equality.ml index 24028b09d..f18de92c0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops diff --git a/tactics/hints.ml b/tactics/hints.ml index 2c2b76412..8f3eb5eb5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -8,7 +8,7 @@ open Pp open Util -open Errors +open CErrors open Names open Vars open Term @@ -1273,7 +1273,7 @@ let pr_hint h = match h.obj with try let (_, env) = Pfedit.get_current_goal_context () in env - with e when Errors.noncritical e -> Global.env () + with e when CErrors.noncritical e -> Global.env () in (str "(*external*) " ++ Pptactic.pr_glb_generic env tac) @@ -1334,7 +1334,7 @@ let pr_applicable_hint () = let pts = get_pftreestate () in let glss = Proof.V82.subgoals pts in match glss.Evd.it with - | [] -> Errors.error "No focused goal." + | [] -> CErrors.error "No focused goal." | g::_ -> pr_hint_term (Goal.V82.concl glss.Evd.sigma g) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index f2c72c2f3..6e24cc469 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -409,7 +409,7 @@ let rec first_match matcher = function let match_eq eqn (ref, hetero) = let ref = try Lazy.force ref - with e when Errors.noncritical e -> raise PatternMatchingFailure + with e when CErrors.noncritical e -> raise PatternMatchingFailure in match kind_of_term eqn with | App (c, [|t; x; y|]) -> diff --git a/tactics/inv.ml b/tactics/inv.ml index 852c2ee7c..bda16b01c 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -440,7 +440,7 @@ let raw_inversion inv_kind id status names = try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in - Errors.errorlabstrm "" msg + CErrors.errorlabstrm "" msg in let IndType (indf,realargs) = find_rectype env sigma t in let evdref = ref sigma in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 63b1a7b54..642bf520b 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml index 2144b75e7..004492e78 100644 --- a/tactics/tactic_matching.ml +++ b/tactics/tactic_matching.ml @@ -103,7 +103,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) = (merged, Id.Map.merge merge lcm lm) let matching_error = - Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.") + CErrors.UserError ("tactic matching" , Pp.str "No matching clauses for match.") let imatching_error = (matching_error, Exninfo.null) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 46145d111..87fdcf14d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -521,7 +521,7 @@ module New = struct try let () = check_evars env sigma_final sigma sigma_initial in tclUNIT x - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> tclZERO e else tclUNIT x @@ -540,7 +540,7 @@ module New = struct Proofview.tclOR (Proofview.tclTIMEOUT n t) begin function (e, info) -> match e with - | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e))) + | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e))) | e -> Proofview.tclZERO ~info e end @@ -551,7 +551,7 @@ module New = struct let hyps = Proofview.Goal.hyps gl in try List.nth hyps (m-1) - with Failure _ -> Errors.error "No such assumption." + with Failure _ -> CErrors.error "No such assumption." let nLastDecls gl n = try List.firstn n (Proofview.Goal.hyps gl) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 61aaef871..e48901314 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -350,7 +350,7 @@ let rename_hyp repl = let () = try let elt = Id.Set.choose (Id.Set.inter dst mods) in - Errors.errorlabstrm "" (pr_id elt ++ str " is already used") + CErrors.errorlabstrm "" (pr_id elt ++ str " is already used") with Not_found -> () in (** All is well *) @@ -1807,8 +1807,8 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) = let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in let rec aux clause = try progress_with_clause flags innerclause clause - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in try aux (clenv_push_prod clause) with NotExtensibleClause -> iraise e in @@ -1838,8 +1838,8 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming clear idstoclear; tac id ]) - with e when with_destruct && Errors.noncritical e -> - let (e, info) = Errors.push e in + with e when with_destruct && CErrors.noncritical e -> + let (e, info) = CErrors.push e in (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) @@ -1987,7 +1987,7 @@ let check_is_type env sigma ty = try let _ = Typing.e_sort_of env evdref ty in !evdref - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> raise (DependsOnBody None) let check_decl env sigma decl = @@ -2001,7 +2001,7 @@ let check_decl env sigma decl = | LocalDef (_,c,_) -> Typing.e_check env evdref c ty in !evdref - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let id = get_id decl in raise (DependsOnBody (Some id)) @@ -3880,7 +3880,7 @@ let compute_elim_sig ?elimc elimt = | Some (LocalAssum (_,ind)) -> let indhd,indargs = decompose_app ind in try {!res with indref = Some (global_of_constr indhd) } - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> error "Cannot find the inductive type of the inductive scheme." let compute_scheme_signature scheme names_info ind_type_guess = @@ -4851,7 +4851,7 @@ let abstract_subproof id gk tac = which is an error irrelevant to the proof system (in fact it means that [e] comes from [tac] failing to yield enough success). Hence it reraises [e]. *) - let (_, info) = Errors.push src in + let (_, info) = CErrors.push src in iraise (e, info) in let const, args = @@ -4911,7 +4911,7 @@ let unify ?(state=full_transparent_state) x y = let sigma = Sigma.to_evar_map sigma in let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma end } diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 9886b263c..a7c32e1d6 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -495,7 +495,7 @@ let coqdep () = add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; @@ -525,6 +525,6 @@ let coqdep () = let _ = try coqdep () - with Errors.UserError(s,p) -> + with CErrors.UserError(s,p) -> let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in Feedback.msg_error pp diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 6f3d8e2b8..eaf938e8c 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -235,7 +235,7 @@ let declare_loading_string () = \n Mltop.set_top\ \n {Mltop.load_obj=\ \n (fun f -> if not (Topdirs.load_file ppf f)\ -\n then Errors.error (\"Could not load plugin \"^f));\ +\n then CErrors.error (\"Could not load plugin \"^f));\ \n Mltop.use_file=Topdirs.dir_use ppf;\ \n Mltop.add_dir=Topdirs.dir_directory;\ \n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ @@ -265,7 +265,7 @@ let create_tmp_main_file modules = let main () = let (options, userfiles) = parse_args () in (* Directories: *) - let () = Envars.set_coqlib ~fail:Errors.error in + let () = Envars.set_coqlib ~fail:CErrors.error in let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in (* Which ocaml compiler to invoke *) let prog = if !opt then "opt" else "ocamlc" in 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 |