From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 01:58:04 +0200 Subject: Remove errorlabstrm in favor of user_err As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch. --- checker/check.ml | 12 +++---- checker/safe_typing.ml | 2 +- dev/doc/changes.txt | 10 ++++-- doc/refman/RefMan-tus.tex | 2 +- engine/logic_monad.ml | 2 +- engine/proofview.ml | 6 ++-- ide/ide_slave.ml | 2 +- interp/constrintern.ml | 2 +- interp/coqlib.ml | 2 +- interp/notation.ml | 4 +-- interp/notation_ops.ml | 4 +-- interp/syntax_def.ml | 2 +- kernel/cbytegen.ml | 2 +- kernel/safe_typing.ml | 4 +-- kernel/term.ml | 4 +-- kernel/term_typing.ml | 2 +- lib/cErrors.ml | 10 +++--- lib/cErrors.mli | 7 ++-- lib/system.ml | 14 ++++---- library/declaremods.ml | 4 +-- library/goptions.ml | 2 +- library/impargs.ml | 8 ++--- library/lib.ml | 12 +++---- library/library.ml | 28 +++++++-------- library/universes.ml | 2 +- ltac/rewrite.ml | 4 +-- ltac/tacenv.ml | 2 +- ltac/tacintern.ml | 2 +- ltac/tacinterp.ml | 4 +-- parsing/egramcoq.ml | 2 +- plugins/cc/cctac.ml | 2 +- plugins/decl_mode/decl_interp.ml | 4 +-- plugins/decl_mode/decl_proof_instr.ml | 6 ++-- plugins/extraction/table.ml | 2 +- plugins/funind/functional_principles_types.ml | 4 +-- plugins/funind/glob_term_to_relation.ml | 4 +-- plugins/funind/indfun.ml | 6 ++-- plugins/funind/indfun_common.ml | 2 +- plugins/funind/invfun.ml | 8 ++--- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.ml | 10 +++--- plugins/rtauto/refl_tauto.ml | 4 +-- plugins/setoid_ring/newring.ml | 10 +++--- plugins/ssrmatching/ssrmatching.ml4 | 2 +- pretyping/cases.ml | 2 +- pretyping/classops.ml | 2 +- pretyping/find_subterm.ml | 2 +- pretyping/indrec.ml | 4 +-- pretyping/inductiveops.ml | 2 +- pretyping/patternops.ml | 2 +- pretyping/pretyping.ml | 6 ++-- pretyping/recordops.ml | 2 +- pretyping/tacred.ml | 14 ++++---- pretyping/unification.ml | 4 +-- printing/prettyp.ml | 6 ++-- proofs/clenv.ml | 22 ++++++------ proofs/logic.ml | 14 ++++---- proofs/pfedit.ml | 2 +- proofs/proof.ml | 4 +-- proofs/proof_global.ml | 2 +- proofs/redexpr.ml | 10 +++--- proofs/refiner.ml | 12 +++---- stm/stm.ml | 14 ++++---- tactics/autorewrite.ml | 2 +- tactics/eauto.ml | 6 ++-- tactics/equality.ml | 10 +++--- tactics/hints.ml | 6 ++-- tactics/hipattern.ml | 2 +- tactics/inv.ml | 4 +-- tactics/leminv.ml | 10 +++--- tactics/tacticals.ml | 2 +- tactics/tactics.ml | 50 +++++++++++++-------------- toplevel/auto_ind_decl.ml | 10 +++--- toplevel/class.ml | 8 ++--- toplevel/classes.ml | 2 +- toplevel/command.ml | 4 +-- toplevel/coqinit.ml | 4 +-- toplevel/ind_tables.ml | 2 +- toplevel/locality.ml | 2 +- toplevel/metasyntax.ml | 18 +++++----- toplevel/mltop.ml | 10 +++--- toplevel/obligations.ml | 8 ++--- toplevel/record.ml | 4 +-- toplevel/vernacentries.ml | 32 ++++++++--------- toplevel/vernacinterp.ml | 4 +-- 85 files changed, 281 insertions(+), 274 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index 863cf7b2c..38d2057eb 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -247,12 +247,12 @@ let locate_qualified_library qid = let error_unmapped_dir qid = let prefix = qid.dirpath in - errorlabstrm "load_absolute_library_from" + user_err "load_absolute_library_from" (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ()) let error_lib_not_found qid = - errorlabstrm "load_absolute_library_from" + user_err "load_absolute_library_from" (str"Cannot find library " ++ pr_path qid ++ str" in loadpath") let try_locate_absolute_library dir = @@ -313,18 +313,18 @@ let intern_from_file (dir, f) = let () = close_in ch in let ch = open_in_bin f in if not (String.equal (Digest.channel ch pos) checksum) then - errorlabstrm "intern_from_file" (str "Checksum mismatch"); + user_err "intern_from_file" (str "Checksum mismatch"); let () = close_in ch in if dir <> sd.md_name then - errorlabstrm "intern_from_file" + user_err "intern_from_file" (name_clash_message dir sd.md_name f); if tasks <> None || discharging <> None then - errorlabstrm "intern_from_file" + user_err "intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin Feedback.msg_notice(str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then - errorlabstrm "intern_from_file" + user_err "intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; Validate.validate !Flags.debug Values.v_univopaques opaque_csts; diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 11cd742ba..c0b3a3e73 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -89,6 +89,6 @@ let import file clib univs digest = let unsafe_import file clib univs digest = let env = !genv in if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps - else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; + else check_imports (user_err"unsafe_import") clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index ac874befd..699130944 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,11 +2,15 @@ = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= +* ML API * + ** Error handling ** -All error functions now take an optional parameter `?loc:Loc.t`. For -functions that used to carry a suffix `_loc`, such suffix has been -dropped. +- All error functions now take an optional parameter `?loc:Loc.t`. For + functions that used to carry a suffix `_loc`, such suffix has been + dropped. + +- `errorlabstrm` has been removed in favor of `user_err`. ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 3e2988676..797b0aded 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -1012,7 +1012,7 @@ the different kinds of errors used in \Coq{} : \fun{val Std.error : string -> 'a} {For simple error messages} -\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a} +\fun{val Std.user_err : ?loc:Loc.t -> string -> std\_ppcmds -> 'a} {See Section~\ref{PrettyPrinter} : this can be used if the user want to display a term or build a complex error message} diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 17ff898b0..e14a2bd39 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -34,7 +34,7 @@ exception Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Timeout -> CErrors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") + | Timeout -> CErrors.user_err "Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e | _ -> Pervasives.raise CErrors.Unhandled diff --git a/engine/proofview.ml b/engine/proofview.ml index 576569cf5..c47c44e22 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -365,7 +365,7 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f let _ = CErrors.register_handler begin function | NoSuchGoals n -> let suffix = !nosuchgoals_hook n in - CErrors.errorlabstrm "" + CErrors.user_err "" (str "No such " ++ str (String.plural n "goal") ++ str "." ++ pr_non_empty_arg (fun x -> x) suffix) | _ -> raise CErrors.Unhandled @@ -451,7 +451,7 @@ let _ = CErrors.register_handler begin function str"Incorrect number of goals" ++ spc() ++ str"(expected "++int i++str(String.plural i " tactic") ++ str")." in - CErrors.errorlabstrm "" errmsg + CErrors.user_err "" errmsg | _ -> raise CErrors.Unhandled end @@ -849,7 +849,7 @@ let tclPROGRESS t = exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Timeout -> CErrors.user_err "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") | _ -> Pervasives.raise CErrors.Unhandled end diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8dda4773e..db0f96715 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -300,7 +300,7 @@ let dirpath_of_string_list s = let id = try Nametab.full_name_module qid with Not_found -> - CErrors.errorlabstrm "Search.interface_search" + CErrors.user_err "Search.interface_search" (str "Module " ++ str path ++ str " not found.") in id diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f4907e92a..82039abd3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -366,7 +366,7 @@ let check_hidden_implicit_parameters id impls = | (Inductive indparams,_,_,_) -> Id.List.mem id indparams | _ -> false) impls then - errorlabstrm "" (strbrk "A parameter of an inductive type " ++ + user_err "" (strbrk "A parameter of an inductive type " ++ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") let push_name_env ?(global_level=false) ntnvars implargs env = diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 588637b76..19f76b972 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -86,7 +86,7 @@ let check_required_library d = (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - errorlabstrm "Coqlib.check_required_library" + user_err "Coqlib.check_required_library" (str "Library " ++ pr_dirpath dir ++ str " has to be required first.") (************************************************************************) diff --git a/interp/notation.ml b/interp/notation.ml index 0c15e91b8..d50045546 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -95,7 +95,7 @@ let declare_scope scope = scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = - errorlabstrm "Notation" + user_err "Notation" (str "Scope " ++ str sc ++ str " is not declared.") let find_scope scope = @@ -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 -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") + | None -> CErrors.user_err "" (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7ab6ebb26..d565f01ba 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -377,7 +377,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = let vars = Id.Map.filter filter nenv.ninterp_var_type in let check_recvar x = if Id.List.mem x found then - errorlabstrm "" (pr_id x ++ + user_err "" (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in @@ -396,7 +396,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then - errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ + user_err "" (strbrk "in the right-hand side, " ++ pr_id x ++ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index f96d8acc1..1e0964dd2 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -30,7 +30,7 @@ let add_syntax_constant kn c onlyparse = let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if Nametab.exists_cci sp then - errorlabstrm "cache_syntax_constant" + user_err "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 2d1ae68f4..9172fdbf0 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 CErrors.errorlabstrm "compile" else + let fn = if fail_on_error then CErrors.user_err "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/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75c..e2ee913a3 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -816,7 +816,7 @@ let export ?except senv dir = try join_safe_environment ?except senv with e -> let e = CErrors.push e in - CErrors.errorlabstrm "export" (CErrors.iprint e) + CErrors.user_err "export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -852,7 +852,7 @@ let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then - CErrors.errorlabstrm "Safe_typing.import" + CErrors.user_err "Safe_typing.import" (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in diff --git a/kernel/term.ml b/kernel/term.ml index 15f187e5c..340730558 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -465,7 +465,7 @@ let rec to_lambda n prod = match kind_of_term prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c - | _ -> errorlabstrm "to_lambda" (mt ()) + | _ -> user_err "to_lambda" (mt ()) let rec to_prod n lam = if Int.equal n 0 then @@ -474,7 +474,7 @@ let rec to_prod n lam = match kind_of_term lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c - | _ -> errorlabstrm "to_prod" (mt ()) + | _ -> user_err "to_prod" (mt ()) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 749b5dbaf..94a05ef67 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -276,7 +276,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in let n = List.length l in - errorlabstrm "" (Pp.(str "The following section " ++ + user_err "" (Pp.(str "The following section " ++ str (String.plural n "variable") ++ str " " ++ str (String.conjugate_verb_to_be n) ++ str " used but not declared:" ++ diff --git a/lib/cErrors.ml b/lib/cErrors.ml index c5f262373..830a9e3ce 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -34,17 +34,17 @@ let is_anomaly = function | _ -> false exception UserError of string * std_ppcmds (* User errors *) -let error string = raise (UserError("_", str string)) -let errorlabstrm l pps = raise (UserError(l,pps)) - -exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *) -let alreadydeclared pps = raise (AlreadyDeclared(pps)) let todo s = prerr_string ("TODO: "^s^"\n") let user_err ?loc s strm = Loc.raise ?loc (UserError (s,strm)) +let error string = user_err "_" (str string) + let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) +exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *) +let alreadydeclared pps = raise (AlreadyDeclared(pps)) + exception Timeout exception Drop exception Quit diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 291c39b84..ad17be393 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -34,10 +34,13 @@ val is_anomaly : exn -> bool tricks with anomalies thanks to it. See rather [noncritical] below. *) exception UserError of string * std_ppcmds -val error : string -> 'a -val errorlabstrm : string -> std_ppcmds -> 'a val user_err : ?loc:Loc.t -> string -> std_ppcmds -> 'a +(** Main error raising primitive. [user_err ?loc c pp] signals an + error [pp] in component [c], with optional location [loc] *) + +val error : string -> 'a +(** [error s] just calls [user_error "_" (str s)] *) exception AlreadyDeclared of std_ppcmds val alreadydeclared : std_ppcmds -> 'a diff --git a/lib/system.ml b/lib/system.ml index af9aa5c07..916c08795 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -132,7 +132,7 @@ let find_file_in_path ?(warn=true) paths filename = let root = Filename.dirname filename in root, filename else - CErrors.errorlabstrm "System.find_file_in_path" + CErrors.user_err "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 @@ -140,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 -> - CErrors.errorlabstrm "System.find_file_in_path" + CErrors.user_err "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) @@ -163,7 +163,7 @@ let is_in_system_path filename = let open_trapping_failure name = try open_out_bin name with e when CErrors.noncritical e -> - CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name) + CErrors.user_err "System.open" (str "Can't open " ++ str name) let warn_cannot_remove_file = CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem" @@ -175,7 +175,7 @@ let try_remove filename = warn_cannot_remove_file filename let error_corrupted file s = - CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") + CErrors.user_err "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -252,7 +252,7 @@ let extern_state magic filename val_0 = let () = try_remove filename in iraise reraise with Sys_error s -> - CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s) + CErrors.user_err "System.extern_state" (str "System error: " ++ str s) let intern_state magic filename = try @@ -261,12 +261,12 @@ let intern_state magic filename = close_in channel; v with Sys_error s -> - CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s) + CErrors.user_err "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} -> - CErrors.errorlabstrm "with_magic_number_check" + CErrors.user_err "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/declaremods.ml b/library/declaremods.ml index b2806a1ac..f388bc8b5 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -166,13 +166,13 @@ let consistency_checks exists dir dirinfo = let globref = try Nametab.locate_dir (qualid_of_dirpath dir) with Not_found -> - errorlabstrm "consistency_checks" + user_err "consistency_checks" (pr_dirpath dir ++ str " should already exist!") in assert (eq_global_dir_reference globref dirinfo) else if Nametab.exists_dir dir then - errorlabstrm "consistency_checks" + user_err "consistency_checks" (pr_dirpath dir ++ str " already exists") let compute_visibility exists i = diff --git a/library/goptions.ml b/library/goptions.ml index 0459417fb..b98cdac6a 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -36,7 +36,7 @@ type option_state = { let nickname table = String.concat " " table let error_undeclared_key key = - errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type") + user_err "Goptions" (str (nickname key) ++ str ": no table or option of this type") (****************************************************************************) (* 1- Tables *) diff --git a/library/impargs.ml b/library/impargs.ml index 6da7e2110..f8990986c 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -339,14 +339,14 @@ let check_correct_manual_implicits autoimps l = List.iter (function | ExplByName id,(b,fi,forced) -> if not forced then - errorlabstrm "" + user_err "" (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then - errorlabstrm "" + user_err "" (str "Bad implicit argument number: " ++ int i ++ str ".") else - errorlabstrm "" + user_err "" (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name.")) l @@ -665,7 +665,7 @@ let check_inclusion l = let check_rigidity isrigid = if not isrigid then - errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") + user_err "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") let projection_implicits env p impls = let pb = Environ.lookup_projection p env in diff --git a/library/lib.ml b/library/lib.ml index 8880a8b15..9d356bca8 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -75,7 +75,7 @@ let classify_segment seg = | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,OpenedModule (ty,_,_,_)) :: _ -> - errorlabstrm "Lib.classify_segment" + user_err "Lib.classify_segment" (str "there are still opened " ++ str (module_kind ty) ++ str "s") | (_,FrozenState _) :: stk -> clean acc stk in @@ -267,7 +267,7 @@ let start_mod is_type export id mp fs = else Nametab.exists_module dir in if exists then - errorlabstrm "open_module" (pr_id id ++ str " already exists"); + user_err "open_module" (pr_id id ++ str " already exists"); add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); path_prefix := prefix; prefix @@ -277,7 +277,7 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in - errorlabstrm "" + user_err "" (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") let end_mod is_type = @@ -322,7 +322,7 @@ let end_compilation_checks dir = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." | OpenedModule (ty,_,_,_) -> - errorlabstrm "Lib.end_compilation_checks" + user_err "Lib.end_compilation_checks" (str "There are some open " ++ str (module_kind ty) ++ str "s.") | _ -> assert false with Not_found -> () @@ -374,7 +374,7 @@ let find_opening_node id = let oname,entry = find_entry_p is_opening_node in let id' = basename (fst oname) in if not (Names.Id.equal id id') then - errorlabstrm "Lib.find_opening_node" + user_err "Lib.find_opening_node" (str "Last block to end has name " ++ pr_id id' ++ str "."); entry with Not_found -> error "There is nothing to end." @@ -525,7 +525,7 @@ let open_section id = let dir = add_dirpath_suffix olddir id in let prefix = dir, (mp, add_dirpath_suffix oldsec id) in if Nametab.exists_section dir then - errorlabstrm "open_section" (pr_id id ++ str " already exists."); + user_err "open_section" (pr_id id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) diff --git a/library/library.ml b/library/library.ml index 0d65b3d0a..8d3916a97 100644 --- a/library/library.ml +++ b/library/library.ml @@ -131,7 +131,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - errorlabstrm "Library.find_library" + user_err "Library.find_library" (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = @@ -329,12 +329,12 @@ let locate_qualified_library ?root ?(warn = true) qid = let error_unmapped_dir qid = let prefix, _ = repr_qualid qid in - errorlabstrm "load_absolute_library_from" + user_err "load_absolute_library_from" (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) let error_lib_not_found qid = - errorlabstrm "load_absolute_library_from" + user_err "load_absolute_library_from" (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") let try_locate_absolute_library dir = @@ -378,7 +378,7 @@ let access_table what tables dp i = let t = try fetch_delayed f with Faulty f -> - errorlabstrm "Library.access_table" + user_err "Library.access_table" (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ str ") is inaccessible or corrupted,\ncannot load some " ++ str what ++ str " in it.\n") @@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = let f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then - errorlabstrm "load_physical_library" + user_err "load_physical_library" (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); @@ -477,7 +477,7 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (dir, None) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); + user_err "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); libs let rec_intern_library libs (dir, f) = @@ -609,7 +609,7 @@ let check_coq_overwriting p id = let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then - errorlabstrm "" + user_err "" (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") @@ -622,7 +622,7 @@ let check_module_name s = (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++ strbrk " is not allowed in module names\n" in - let err c = errorlabstrm "" (msg c) in + let err c = user_err "" (msg c) in match String.get s 0 with | 'a' .. 'z' | 'A' .. 'Z' -> for i = 1 to (String.length s)-1 do @@ -658,10 +658,10 @@ let load_library_todo f = let tasks, _, _ = System.marshal_in_segment f ch in let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; - if tasks = None then errorlabstrm "restart" (str"not a .vio file"); - if s2 = None then errorlabstrm "restart" (str"not a .vio file"); - if s3 = None then errorlabstrm "restart" (str"not a .vio file"); - if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file"); + if tasks = None then user_err "restart" (str"not a .vio file"); + if s2 = None then user_err "restart" (str"not a .vio file"); + if s3 = None then user_err "restart" (str"not a .vio file"); + if pi3 (Option.get s2) then user_err "restart" (str"not a .vio file"); longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) @@ -677,7 +677,7 @@ let current_deps () = let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = - errorlabstrm "" + user_err "" (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") @@ -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 CErrors.errorlabstrm "library" + if not(is_done_or_todo i x) then CErrors.user_err "library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; let sd = { diff --git a/library/universes.ml b/library/universes.ml index db95607f1..04b39937e 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -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 - CErrors.errorlabstrm "Universes" + CErrors.user_err "Universes" (str "Polymorphic constant expected " ++ int len2 ++ str" levels but was given " ++ int len1) else () diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 47c78ae5c..e0583370a 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1508,7 +1508,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul Evar.Set.fold (fun ev acc -> if not (Evd.is_defined acc ev) then - errorlabstrm "rewrite" + user_err "rewrite" (str "Unsolved constraint remaining: " ++ spc () ++ Evd.pr_evar_info (Evd.find acc ev)) else Evd.remove acc ev) @@ -1647,7 +1647,7 @@ let cl_rewrite_clause_strat progress strat clause = (fun gl -> try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl with RewriteFailure e -> - errorlabstrm "" (str"setoid rewrite failed: " ++ e) + user_err "" (str"setoid rewrite failed: " ++ e) | Refiner.FailError (n, pp) -> tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)) diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index c709ab114..5808feeba 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -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 -> - CErrors.errorlabstrm "" + CErrors.user_err "" (str "The tactic " ++ pr_tacname s ++ str " is not installed.") (***************************************************************************) diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index dc216da11..a1d34b53f 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -748,7 +748,7 @@ let print_ltac id = ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined with Not_found -> - errorlabstrm "print_ltac" + user_err "print_ltac" (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") (** Registering *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 76c46ea7c..b1f554eaa 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -168,7 +168,7 @@ module Value = struct let pr_v = Pptactic.pr_value Pptactic.ltop v in let Val.Dyn (tag, _) = v in let tag = Val.pr tag in - errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag + user_err "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag ++ str " while type " ++ Val.pr wit ++ str " was expected.") let unbox wit v ans = match ans with @@ -1870,7 +1870,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma, c) = interp_constr ist env sigma c in Sigma.Unsafe.of_pair (c, sigma) with e when to_catch e (* Hack *) -> - errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") + user_err "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") end } in Tactics.change (Some op) c_interp (interp_clause ist env sigma cl) end } diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 65d49cb45..7d3cb7e49 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -71,7 +71,7 @@ let error_level_assoc p current expected = | Extend.LeftA -> str "left" | Extend.RightA -> str "right" | Extend.NonA -> str "non" in - errorlabstrm "" + user_err "" (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ pr_assoc expected ++ str " associative.") diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index fd46d8069..6ed678176 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -456,7 +456,7 @@ let cc_tactic depth additionnal_terms = end } let cc_fail gls = - errorlabstrm "Congruence" (Pp.str "congruence failed.") + user_err "Congruence" (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 49843d828..9ed5c61e2 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let _ = let expected = mib.Declarations.mind_nparams - num_params in if not (Int.equal (List.length params) expected) then - errorlabstrm "suppose it is" + user_err "suppose it is" (str "Wrong number of extra arguments: " ++ (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ str "expected.") in @@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> if not (Id.List.mem rec_occ pat_vars) then - errorlabstrm "suppose it is" + user_err "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); Glob_term.GSort(Loc.ghost,GProp) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 97c9d5f4a..9510ba384 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -43,7 +43,7 @@ let clear ids { it = goal; sigma } = let (hyps, concl) = try Evarutil.clear_hyps_in_evi env evdref sign cl ids with Evarutil.ClearDependencyError (id, _) -> - errorlabstrm "" (str "Cannot clear " ++ pr_id id) + user_err "" (str "Cannot clear " ++ pr_id id) in let sigma = !evdref in let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in @@ -1082,12 +1082,12 @@ let thesis_for obj typ per_info env= let cind,all_args=decompose_app typ in let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then - errorlabstrm "thesis_for" + user_err "thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then - errorlabstrm "thesis_for" + user_err "thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ff66d915f..3c26c4710 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -293,7 +293,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = errorlabstrm "Extraction" s +let err s = user_err "Extraction" s let warn_extraction_axiom_to_realize = CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5e72b8672..f4daa0323 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -609,7 +609,7 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - errorlabstrm "FunInd.build_scheme" + user_err "FunInd.build_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in @@ -643,7 +643,7 @@ let build_case_scheme fa = let (_,f,_) = fa in try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) with Not_found -> - errorlabstrm "FunInd.build_case_scheme" + user_err "FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 5548833d6..9902b0128 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -630,7 +630,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ + user_err "" (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in @@ -662,7 +662,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ + user_err "" (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 4f183b3a1..943ebc9fc 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -42,7 +42,7 @@ let functional_induction with_clean c princl pat = let finfo = (* we first try to find out a graph on f *) try find_Function_infos c' with Not_found -> - errorlabstrm "" (str "Cannot find induction information on "++ + user_err "" (str "Cannot find induction information on "++ Printer.pr_lconstr (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with @@ -70,7 +70,7 @@ let functional_induction with_clean c princl pat = (b,a) (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) - errorlabstrm "" (str "Cannot find induction principle for " + user_err "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') @@ -321,7 +321,7 @@ let error_error names e = in match e with | Building_graph e -> - errorlabstrm "" + user_err "" (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f56e92414..a1c94f8cb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -110,7 +110,7 @@ let const_of_id id = in try Constrintern.locate_reference princ_ref with Not_found -> - CErrors.errorlabstrm "IndFun.const_of_id" + CErrors.user_err "IndFun.const_of_id" (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 26fc88a60..ee1232013 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1043,19 +1043,19 @@ let invfun qhyp f g = functional_inversion kn hid f2 f_correct g with | Failure "" -> - errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") + user_err "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") | Option.IsNone -> if do_observe () then error "Cannot use equivalence with graph for any side of the equality" - else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) | Not_found -> if do_observe () then error "No graph found for any side of equality" - else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) end - | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ") + | _ -> user_err "" (Ppconstr.pr_id hid ++ str " must be an equality ") end) qhyp end diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index de4210af5..0b93a909a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -901,7 +901,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = locate_constant f_ref in try find_Function_infos (kn_of_id id) with Not_found -> - errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme") + user_err "indfun" (Nameops.pr_id id ++ str " has no functional scheme") (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 62f307115..7745e8498 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -307,7 +307,7 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then errorlabstrm "Recdef.check_not_nested" + then user_err "Recdef.check_not_nested" (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t @@ -327,7 +327,7 @@ let check_not_nested forbidden e = try check_not_nested e with UserError(_,p) -> - errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) + user_err "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = 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 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) + user_err "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) -> begin @@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = 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 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) + user_err "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) -> begin @@ -478,7 +478,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos - | Case _ -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | Case _ -> user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info) end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 4ed907951..9cfcb0fb7 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -263,7 +263,7 @@ let rtauto_tac gls= let _= if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp - then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in + then user_err "rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= @@ -282,7 +282,7 @@ let rtauto_tac gls= let prf = try project (search_fun (init_state [] formula)) with Not_found -> - errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in + user_err "rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in let _ = if !verbose then begin diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 90f5f8e63..7450aa23e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -79,7 +79,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - errorlabstrm"lookup_map"(str"map "++qs map++str"not found") + user_err"lookup_map"(str"map "++qs map++str"not found") let protect_red map env sigma c = kl (create_clos_infos all env) @@ -348,13 +348,13 @@ let find_ring_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "ring" + user_err "ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; (try ring_for_carrier ty with Not_found -> - errorlabstrm "ring" + user_err "ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false @@ -828,13 +828,13 @@ let find_field_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "field" + user_err "field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; (try field_for_carrier ty with Not_found -> - errorlabstrm "field" + user_err "field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 536c6ff4b..199c26363 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -61,7 +61,7 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = CErrors.errorlabstrm "ssrmatching" +let errorstrm = CErrors.user_err "ssrmatching" let loc_error loc msg = CErrors.user_err ~loc msg (str msg) let ppnl = Feedback.msg_info diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 85c518019..18ad2ed3d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -503,7 +503,7 @@ let set_used_pattern eqn = eqn.used := true let extract_rhs pb = match pb.mat with - | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion()) + | [] -> user_err "build_leaf" (msg_may_need_inversion()) | eqn::_ -> set_used_pattern eqn; eqn.rhs diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 4f265e76c..92a0ca988 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -538,7 +538,7 @@ let inheritance_graph () = let coercion_of_reference r = let ref = Nametab.global r in if not (coercion_exists ref) then - errorlabstrm "try_add_coercion" + user_err "try_add_coercion" (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion."); ref diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 4caa1e992..c7909a3c7 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -35,7 +35,7 @@ let explain_occurrence_error = function | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id let error_occurrences_error e = - errorlabstrm "" (explain_occurrence_error e) + user_err "" (explain_occurrence_error e) let error_invalid_occurrence occ = error_occurrences_error (InvalidOccurrence occ) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 39aeb41f7..0061d8ae9 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -55,7 +55,7 @@ let is_private mib = let check_privacy_block mib = if is_private mib then - errorlabstrm ""(str"case analysis on a private inductive type") + user_err ""(str"case analysis on a private inductive type") (**********************************************************************) (* Building case analysis schemes *) @@ -594,7 +594,7 @@ let lookup_eliminator ind_sp s = (* using short name (e.g. for "eq_rec") *) try Nametab.locate (qualid_of_ident id) with Not_found -> - errorlabstrm "default_elim" + user_err "default_elim" (strbrk "Cannot find the elimination combinator " ++ pr_id id ++ strbrk ", the elimination of the inductive definition " ++ pr_global_env Id.Set.empty (IndRef ind_sp) ++ diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 214e19fec..cb69ab36f 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -355,7 +355,7 @@ let make_case_or_project env indf ci pred c branches = let mib, _ = Inductive.lookup_mind_specif env ind in if (* dependent *) not (noccurn 1 t) && not (has_dependent_elim mib) then - errorlabstrm "make_case_or_project" + user_err "make_case_or_project" Pp.(str"Dependent case analysis not allowed" ++ str" on inductive type " ++ Names.MutInd.print (fst ind)) in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 99c3772db..aa795106a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -204,7 +204,7 @@ let error_instantiate_pattern id l = | [_] -> "is" | _ -> "are" in - errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id + user_err "" (str "Cannot substitute the term bound to " ++ pr_id id ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8b0bdb009..cdb39207e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -390,7 +390,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function try Name (Id.Map.find id ltac_idents) with Not_found -> if Id.Map.mem id ltac_genargs then - errorlabstrm "" (str"Ltac variable"++spc()++ pr_id id ++ + user_err "" (str"Ltac variable"++spc()++ pr_id id ++ spc()++str"is not bound to an identifier."++spc()++ str"It cannot be used in a binder.") else n @@ -411,14 +411,14 @@ let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in try mkRel (pi1 (lookup_rel_id id' (rel_context env))) with Not_found -> - errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ + user_err "" (str "Ltac variable " ++ pr_id id0 ++ str " depends on pattern variable name " ++ pr_id id ++ str " which is not bound in current context.") let protected_get_type_of env sigma c = try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> - errorlabstrm "" + user_err "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 284af0cb1..945ef5daa 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -291,7 +291,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) (*s High-level declaration of a canonical structure *) let error_not_structure ref = - errorlabstrm "object_declare" + user_err "object_declare" (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.") let check_and_decompose_canonical_structure ref = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 820a81b5d..67819dc98 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -38,7 +38,7 @@ exception Elimconst exception Redelimination let error_not_evaluable r = - errorlabstrm "error_not_evaluable" + user_err "error_not_evaluable" (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ str "to an evaluable reference.") @@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> incr pos; if ok then begin if Option.has_some nested then - errorlabstrm "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str "."); + user_err "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str "."); (* Skip inner occurrences for stable counting of occurrences *) if locs != [] then ignore (traverse_below (Some (!pos-1)) envc t); @@ -1159,13 +1159,13 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> let check_privacy env ind = let spec = Inductive.lookup_mind_specif env (fst ind) in if Inductive.is_private spec then - errorlabstrm "" (str "case analysis on a private type.") + user_err "" (str "case analysis on a private type.") else ind let check_not_primitive_record env ind = let spec = Inductive.lookup_mind_specif env (fst ind) in if Inductive.is_primitive_record spec then - errorlabstrm "" (str "case analysis on a primitive record type: " ++ + user_err "" (str "case analysis on a primitive record type: " ++ str "use projections or let instead.") else ind @@ -1182,14 +1182,14 @@ let reduce_to_ind_gen allow_product env sigma t = if allow_product then elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else - errorlabstrm "" (str"Not an inductive definition.") + user_err "" (str"Not an inductive definition.") | _ -> (* Last chance: we allow to bypass the Opaque flag (as it was partially the case between V5.10 and V8.1 *) let t' = whd_all env sigma t in match kind_of_term (fst (decompose_app t')) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) - | _ -> errorlabstrm "" (str"Not an inductive product.") + | _ -> user_err "" (str"Not an inductive product.") in elimrec env t [] @@ -1239,7 +1239,7 @@ let one_step_reduce env sigma c = applist (redrec (c,[])) let error_cannot_recognize ref = - errorlabstrm "" + user_err "" (str "Cannot recognize a statement based on " ++ Nametab.pr_global_env Id.Set.empty ref ++ str".") diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0c1ce0d2f..5e3c3c259 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1586,7 +1586,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context x (named_context env) then - errorlabstrm "Unification.make_abstraction_core" + user_err "Unification.make_abstraction_core" (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else x @@ -1600,7 +1600,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = if indirectly_dependent c d depdecls then (* Told explicitly not to abstract over [d], but it is dependent *) let id' = indirect_dependency d depdecls in - errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id' + user_err "" (str "Cannot abstract over " ++ Nameops.pr_id id' ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp ++ str ".") else diff --git a/printing/prettyp.ml b/printing/prettyp.ml index a7742d866..e2fefa5c8 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -736,7 +736,7 @@ let print_any_name = function let open Context.Named.Declaration in str |> Global.lookup_named |> set_id str |> print_named_decl with Not_found -> - errorlabstrm + user_err "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") let print_name = function @@ -831,7 +831,7 @@ let index_of_class cl = try fst (class_info cl) with Not_found -> - errorlabstrm "index_of_class" + user_err "index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") let print_path_between cls clt = @@ -841,7 +841,7 @@ let print_path_between cls clt = try lookup_path_between_class (i,j) with Not_found -> - errorlabstrm "index_cl_of_id" + user_err "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0a90e0dbd..0ee13bb63 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -155,7 +155,7 @@ let error_incompatible_inst clenv mv = let na = meta_name clenv.evd mv in match na with Name id -> - errorlabstrm "clenv_assign" + user_err "clenv_assign" (str "An incompatible instantiation has already been found for " ++ pr_id id) | _ -> @@ -417,11 +417,11 @@ let qhyp_eq h1 h2 = match h1, h2 with let check_bindings bl = match List.duplicates qhyp_eq (List.map pi2 bl) with | NamedHyp s :: _ -> - errorlabstrm "" + user_err "" (str "The variable " ++ pr_id s ++ str " occurs more than once in binding list."); | AnonHyp n :: _ -> - errorlabstrm "" + user_err "" (str "The position " ++ int n ++ str " occurs more than once in binding list.") | [] -> () @@ -435,7 +435,7 @@ let explain_no_such_bound_variable evd id = if na != Anonymous then out_name na :: l else l in let mvl = List.fold_left fold [] (Evd.meta_list evd) in - errorlabstrm "Evd.meta_with_name" + user_err "Evd.meta_with_name" (str"No such bound variable " ++ pr_id id ++ (if mvl == [] then str " (no bound variables at all in the expression)." else @@ -460,7 +460,7 @@ let meta_with_name evd id = | ([n],_|_,[n]) -> n | _ -> - errorlabstrm "Evd.meta_with_name" + user_err "Evd.meta_with_name" (str "Binder name \"" ++ pr_id id ++ strbrk "\" occurs more than once in clause.") @@ -469,12 +469,12 @@ let meta_of_binder clause loc mvs = function | AnonHyp n -> try List.nth mvs (n-1) with (Failure _|Invalid_argument _) -> - errorlabstrm "" (str "No such binder.") + user_err "" (str "No such binder.") let error_already_defined b = match b with | NamedHyp id -> - errorlabstrm "" + user_err "" (str "Binder name \"" ++ pr_id id ++ str"\" already defined with incompatible value.") | AnonHyp n -> @@ -527,7 +527,7 @@ let clenv_constrain_last_binding c clenv = clenv_assign_binding clenv k c let error_not_right_number_missing_arguments n = - errorlabstrm "" + user_err "" (strbrk "Not the right number of missing arguments (expected " ++ int n ++ str ").") @@ -641,7 +641,7 @@ let explain_no_such_bound_variable holes id = | [id] -> str "(possible name is: " ++ pr_id id ++ str ")." | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")." in - errorlabstrm "" (str "No such bound variable " ++ pr_id id ++ expl) + user_err "" (str "No such bound variable " ++ pr_id id ++ expl) let evar_with_name holes id = let map h = match h.hole_name with @@ -653,7 +653,7 @@ let evar_with_name holes id = | [] -> explain_no_such_bound_variable holes id | [h] -> h.hole_evar | _ -> - errorlabstrm "" + user_err "" (str "Binder name \"" ++ pr_id id ++ str "\" occurs more than once in clause.") @@ -664,7 +664,7 @@ let evar_of_binder holes = function let h = List.nth holes (pred n) in h.hole_evar with e when CErrors.noncritical e -> - errorlabstrm "" (str "No such binder.") + user_err "" (str "No such binder.") let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in diff --git a/proofs/logic.ml b/proofs/logic.ml index aa0b9bac6..9f34f5cf6 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -151,7 +151,7 @@ let reorder_context env sign ord = | top::ord' when mem_q top moved_hyps -> let ((d,h),mh) = find_q top moved_hyps in if occur_vars_in_decl env h d then - errorlabstrm "reorder_context" + user_err "reorder_context" (str "Cannot move declaration " ++ pr_id top ++ spc() ++ str "before " ++ pr_sequence pr_id @@ -182,7 +182,7 @@ let check_decl_position env sign d = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then - errorlabstrm "Logic.check_decl_position" + user_err "Logic.check_decl_position" (str "Cannot create self-referring hypothesis " ++ pr_id x); x::deps @@ -252,7 +252,7 @@ let move_hyp toleft (left,declfrom,right) hto = if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ + user_err "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") @@ -287,7 +287,7 @@ let move_hyp toleft (left,declfrom,right) hto = variables only in Application and Case *) let error_unsupported_deep_meta c = - errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++ + user_err "" (strbrk "Application of lemmas whose beta-iota normal " ++ strbrk "form contains metavariables deep inside the term is not " ++ strbrk "supported; try \"refine\" instead.") @@ -498,10 +498,10 @@ let convert_hyp check sign sigma d = let _,c,ct = to_tuple d' in let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then - errorlabstrm "Logic.convert_hyp" + user_err "Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then - errorlabstrm "Logic.convert_hyp" + user_err "Logic.convert_hyp" (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sign d; d) in @@ -534,7 +534,7 @@ let prim_refiner r sigma goal = t,cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then - errorlabstrm "Logic.prim_refiner" + user_err "Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in let (sg2,ev2,sigma) = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e4bae2012..b86582def 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -131,7 +131,7 @@ let solve ?with_end_tac gi info_lvl tac pr = | CList.IndexOutOfRange -> match gi with | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in - CErrors.errorlabstrm "" msg + CErrors.user_err "" msg | _ -> assert false let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) diff --git a/proofs/proof.ml b/proofs/proof.ml index 5fe29653d..2e5330b4b 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -68,9 +68,9 @@ let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> CErrors.error "This proof is focused, but cannot be unfocused this way" | NoSuchGoals (i,j) when Int.equal i j -> - CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").") + CErrors.user_err "Focus" Pp.(str"No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - CErrors.errorlabstrm "Focus" Pp.( + CErrors.user_err "Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) | FullyUnfocused -> CErrors.error "The proof is not focused" diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7b43b64ef..107a3a7e5 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -519,7 +519,7 @@ module Bullet = struct (function | FailedBullet (b,sugg) -> let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in - CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg) + CErrors.user_err "Focus" (prefix ++ suggest_on_error sugg) | _ -> raise CErrors.Unhandled) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 8a9ce4f94..cafd46849 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -73,7 +73,7 @@ let set_strategy_one ref l = let cb = Global.lookup_constant sp in (match cb.const_body with | OpaqueDef _ -> - errorlabstrm "set_transparent_const" + user_err "set_transparent_const" (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); @@ -175,19 +175,19 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then errorlabstrm "Redexpr.declare_reduction" + then user_err "Redexpr.declare_reduction" (str "There is already a reduction expression of name " ++ str s) else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) + then user_err "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) |_ -> () let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then errorlabstrm "Redexpr.decl_red_expr" + then user_err "Redexpr.decl_red_expr" (str "There is already a reduction expression of name " ++ str s) else begin check_custom e; @@ -247,7 +247,7 @@ let reduction_of_red_expr env = with Not_found -> (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> - errorlabstrm "Redexpr.reduction_of_red_expr" + user_err "Redexpr.reduction_of_red_expr" (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ebd30820b..65a889882 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -60,7 +60,7 @@ let tclIDTAC_MESSAGE s gls = Feedback.msg_info (hov 0 s); tclIDTAC gls (* General failure tactic *) -let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) +let tclFAIL_s s gls = user_err "Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) exception FailError of int * std_ppcmds Lazy.t @@ -82,7 +82,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = let nf = Array.length tacfi in let nl = Array.length tacli in let ng = List.length gs in - if ng apply_sig_tac sigr (if i=ng-nl then tacli.(nl-ng+i) else tac)) @@ -164,14 +164,14 @@ the goal unchanged *) let tclWEAK_PROGRESS tac ptree = let rslt = tac ptree in if Goal.V82.weak_progress rslt ptree then rslt - else errorlabstrm "Refiner.WEAK_PROGRESS" (str"Failed to progress.") + else user_err "Refiner.WEAK_PROGRESS" (str"Failed to progress.") (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged *) let tclPROGRESS tac ptree = let rslt = tac ptree in if Goal.V82.progress rslt ptree then rslt - else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.") + else user_err "Refiner.PROGRESS" (str"Failed to progress.") (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals, one of them being identical to the original goal *) @@ -182,7 +182,7 @@ let tclNOTSAMEGOAL (tac : tactic) goal = let rslt = tac goal in let {it=gls;sigma=sigma} = rslt in if List.exists (same_goal goal sigma) gls - then errorlabstrm "Refiner.tclNOTSAMEGOAL" + then user_err "Refiner.tclNOTSAMEGOAL" (str"Tactic generated a subgoal identical to the original goal.") else rslt @@ -316,7 +316,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) let tclDO n t = let rec dorec k = - if k < 0 then errorlabstrm "Refiner.tclDO" + if k < 0 then user_err "Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); if Int.equal k 0 then tclIDTAC else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) diff --git a/stm/stm.ml b/stm/stm.ml index 9f86597dc..ff4688480 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1038,7 +1038,7 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - CErrors.errorlabstrm "undo_vernac_classifier" + CErrors.user_err "undo_vernac_classifier" (str "Cannot undo") end (* }}} *) @@ -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 - CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name); + CErrors.user_err "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 -> - CErrors.errorlabstrm "STM" + CErrors.user_err "STM" (str "Unknown proof block delimiter " ++ str name) ) (****************************** THE SCHEDULER *********************************) @@ -1706,7 +1706,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) Evd.(evar_context g)) then - CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^ + CErrors.user_err "STM" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin let (i, ast) = r_ast in @@ -1719,7 +1719,7 @@ 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 CErrors.errorlabstrm "STM" (str"The solution is not ground") + else CErrors.user_err "STM" (str"The solution is not ground") end) () with e when CErrors.noncritical e -> RespError (CErrors.print e) @@ -2056,7 +2056,7 @@ let known_state ?(redefine_qed=false) ~cache id = | _ -> assert false end with Not_found -> - CErrors.errorlabstrm "STM" + CErrors.user_err "STM" (str "Unknown proof block delimiter " ++ str name) in @@ -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 - CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs"); + CErrors.user_err "stm" (str"Cannot dump a vio with open proofs"); Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo (Global.opaque_tables ()) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 3257d406a..b898ceb04 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -65,7 +65,7 @@ let raw_find_base bas = String.Map.find bas !rewtab let find_base bas = try raw_find_base bas with Not_found -> - errorlabstrm "AutoRewrite" + user_err "AutoRewrite" (str "Rewriting base " ++ str bas ++ str " does not exist.") let find_rewrites bas = diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2eca1e597..dcf3dea10 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -98,7 +98,7 @@ let prolog_tac l n = let l = List.map map l in try (prolog l n gl) with UserError ("Refiner.tclFIRST",_) -> - errorlabstrm "Prolog.prolog" (str "Prolog failed.") + user_err "Prolog.prolog" (str "Prolog failed.") end open Auto @@ -431,7 +431,7 @@ let cons a l = a :: l let autounfolds db occs cls gl = let unfolds = List.concat (List.map (fun dbname -> let db = try searchtable_map dbname - with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) + with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname) in let (ids, csts) = Hint_db.unfolds db in let hyps = pf_ids_of_hyps gl in @@ -498,7 +498,7 @@ let autounfold_one db cl = let st = List.fold_left (fun (i,c) dbname -> let db = try searchtable_map dbname - with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) + with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname) in let (ids, csts) = Hint_db.unfolds db in (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db diff --git a/tactics/equality.ml b/tactics/equality.ml index 2c97cf442..4391a96b1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -359,7 +359,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = let _ = Global.lookup_constant c1' in c1' with Not_found -> - errorlabstrm "Equality.find_elim" + user_err "Equality.find_elim" (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".") end | _ -> destConstRef pr1 @@ -888,7 +888,7 @@ let build_selector env sigma dirn c ind special default = on (c bool true) = (c bool false) CP : changed assert false in a more informative error *) - errorlabstrm "Equality.construct_discriminator" + user_err "Equality.construct_discriminator" (str "Cannot discriminate on inductive constructors with \ dependent types.") in let (indp,_) = dest_ind_family indf in @@ -974,7 +974,7 @@ let apply_on_clause (f,t) clause = let argmv = (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in + | _ -> user_err "" (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = @@ -1052,7 +1052,7 @@ let discrEverywhere with_evars = else (* <= 8.2 compat *) tryAllHypsAndConcl (discrSimpleClause with_evars)) (* (fun gls -> - errorlabstrm "DiscrEverywhere" (str"No discriminable equalities.")) + user_err "DiscrEverywhere" (str"No discriminable equalities.")) *) let discr_tac with_evars = function | None -> discrEverywhere with_evars @@ -1725,7 +1725,7 @@ let subst_one_var dep_proof_ok x = let hyps = Proofview.Goal.hyps gl in let test hyp _ = is_eq_x gl x hyp in Context.Named.fold_outside test ~init:() hyps; - errorlabstrm "Subst" + user_err "Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ str".") with FoundHyp res -> res in diff --git a/tactics/hints.ml b/tactics/hints.ml index 8f3eb5eb5..e706316d7 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -632,7 +632,7 @@ let current_pure_db () = List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable)) let error_no_such_hint_database x = - errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".") + user_err "Hints" (str "No such Hint database: " ++ str x ++ str ".") (**************************************************************************) (* Definition of the summary *) @@ -774,7 +774,7 @@ let make_resolves env sigma flags pri poly ?name cr = [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name] in if List.is_empty ents then - errorlabstrm "Hint" + user_err "Hint" (pr_lconstr c ++ spc() ++ (if pi1 flags then str"cannot be used as a hint." else str "can be used as a hint only for eauto.")); @@ -817,7 +817,7 @@ let make_mode ref m = let n = List.length ctx in let m' = Array.of_list m in if not (n == Array.length m') then - errorlabstrm "Hint" + user_err "Hint" (pr_global ref ++ str" has " ++ int n ++ str" arguments while the mode declares " ++ int (Array.length m')) else m' diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6e24cc469..aee3bc45d 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -450,7 +450,7 @@ let find_this_eq_data_decompose gl eqn = try (*first_match (match_eq eqn) inversible_equalities*) find_eq_data eqn with PatternMatchingFailure -> - errorlabstrm "" (str "No primitive equality found.") in + user_err "" (str "No primitive equality found.") in let eq_args = try extract_eq_args gl eq_args with PatternMatchingFailure -> diff --git a/tactics/inv.ml b/tactics/inv.ml index bda16b01c..a7f5ded5b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -76,7 +76,7 @@ let make_inv_predicate env evd indf realargs id status concl = (hyps_arity,concl) | Dep dflt_concl -> if not (occur_var env id concl) then - errorlabstrm "make_inv_predicate" + user_err "make_inv_predicate" (str "Current goal does not depend on " ++ pr_id id ++ str"."); (* We abstract the conclusion of goal with respect to realargs and c to * be concl in order to rewrite and have @@ -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 - CErrors.errorlabstrm "" msg + CErrors.user_err "" 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 642bf520b..e83093b0c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -183,7 +183,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let ind = try find_rectype env sigma i with Not_found -> - errorlabstrm "inversion_scheme" (no_inductive_inconstr env sigma i) + user_err "inversion_scheme" (no_inductive_inconstr env sigma i) in let (invEnv,invGoal) = compute_first_inversion_scheme env sigma ind sort dep_option @@ -193,7 +193,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = (global_vars env invGoal) (ids_of_named_context (named_context invEnv))); (* - errorlabstrm "lemma_inversion" + user_err "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in @@ -248,7 +248,7 @@ let add_inversion_lemma_exn na com comsort bool tac = add_inversion_lemma na env sigma c sort bool tac with | UserError ("Case analysis",s) -> (* Reference to Indrec *) - errorlabstrm "Inv needs Nodep Prop Set" s + user_err "Inv needs Nodep Prop Set" s (* ================================= *) (* Applying a given inversion lemma *) @@ -261,10 +261,10 @@ let lemInv id c gls = Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls with | NoSuchBinding -> - errorlabstrm "" + user_err "" (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma.")) | UserError (a,b) -> - errorlabstrm "LemInv" + user_err "LemInv" (str "Cannot refine current goal with the lemma " ++ pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 28a7b634c..c9af1f11c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -643,7 +643,7 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - errorlabstrm "Tacticals.general_elim_then_using" + user_err "Tacticals.general_elim_then_using" (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ef66e6146..16643b6a7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -183,7 +183,7 @@ let introduction ?(check=true) id = let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in let () = if check && mem_named_context id hyps then - errorlabstrm "Tactics.introduction" + user_err "Tactics.introduction" (str "Variable " ++ pr_id id ++ str " is already declared.") in match kind_of_term (whd_evar sigma concl) with @@ -255,7 +255,7 @@ let clear_dependency_msg env sigma id = function Printer.pr_existential env sigma ev ++ str"." let error_clear_dependency env sigma id err = - errorlabstrm "" (clear_dependency_msg env sigma id err) + user_err "" (clear_dependency_msg env sigma id err) let replacing_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> @@ -269,7 +269,7 @@ let replacing_dependency_msg env sigma id = function Printer.pr_existential env sigma ev ++ str"." let error_replacing_dependency env sigma id err = - errorlabstrm "" (replacing_dependency_msg env sigma id err) + user_err "" (replacing_dependency_msg env sigma id err) (* This tactic enables the user to remove hypotheses from the signature. * Some care is taken to prevent him from removing variables that are @@ -350,7 +350,7 @@ let rename_hyp repl = let () = try let elt = Id.Set.choose (Id.Set.inter dst mods) in - CErrors.errorlabstrm "" (pr_id elt ++ str " is already used") + CErrors.user_err "" (pr_id elt ++ str " is already used") with Not_found -> () in (** All is well *) @@ -508,7 +508,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> if not (eq_mind sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; if mem_named_context f (named_context_of_val sign) then - errorlabstrm "Logic.prim_refiner" + user_err "Logic.prim_refiner" (str "Name " ++ pr_id f ++ str " already used in the environment"); mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in @@ -599,7 +599,7 @@ let pf_reduce_decl redfun where decl gl = match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str " has no value."); + user_err "" (pr_id id ++ str " has no value."); LocalAssum (id,redfun' ty) | LocalDef (id,b,ty) -> let b' = if where != InHypTypeOnly then redfun' b else b in @@ -700,7 +700,7 @@ let pf_e_reduce_decl redfun where decl gl = match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str " has no value."); + user_err "" (pr_id id ++ str " has no value."); let Sigma (ty', sigma, p) = redfun sigma ty in Sigma (LocalAssum (id, ty'), sigma, p) | LocalDef (id,b,ty) -> @@ -740,7 +740,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str " has no value."); + user_err "" (pr_id id ++ str " has no value."); let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in Sigma (LocalAssum (id, ty'), sigma, p) | LocalDef (id,b,ty) -> @@ -778,12 +778,12 @@ let check_types env sigma mayneedglobalcheck deep newc origc = isSort (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else - errorlabstrm "convert-check-hyp" (str "Types are incompatible.") + user_err "convert-check-hyp" (str "Types are incompatible.") else sigma end else if not (isSort (whd_all env sigma t1)) then - errorlabstrm "convert-check-hyp" (str "Not a type.") + user_err "convert-check-hyp" (str "Not a type.") else sigma (* Now we introduce different instances of the previous tacticals *) @@ -792,7 +792,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun en let sigma = Sigma.to_evar_map sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in - if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); + if not b then user_err "convert-check-hyp" (str "Not convertible."); Sigma.Unsafe.of_pair (t', sigma) end } @@ -883,7 +883,7 @@ let reduce redexp cl = let unfold_constr = function | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp] | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id] - | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.") + | _ -> user_err "unfold_constr" (str "Cannot unfold a non-constant.") (*******************************************) (* Introduction tactics *) @@ -1078,7 +1078,7 @@ let depth_of_quantified_hypothesis red h gl = match lookup_hypothesis_as_renamed_gen red h gl with | Some depth -> depth | None -> - errorlabstrm "lookup_quantified_hypothesis" + user_err "lookup_quantified_hypothesis" (str "No " ++ msg_quantified_hypothesis h ++ strbrk " in current goal" ++ (if red then strbrk " even after head-reduction" else mt ()) ++ @@ -1227,7 +1227,7 @@ let cut c = let error_uninstantiated_metas t clenv = let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta") - in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") + in user_err "" (str "Cannot find an instance for " ++ pr_id id ++ str".") let check_unresolved_evars_of_metas sigma clenv = (* This checks that Metas turned into Evars by *) @@ -1360,7 +1360,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags let indmv = (match kind_of_term (nth_arg i elimclause.templval.rebus) with | Meta mv -> mv - | _ -> errorlabstrm "elimination_clause" + | _ -> user_err "elimination_clause" (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in @@ -1525,7 +1525,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) try match List.remove Int.equal indmv (clenv_independent elimclause) with | [a] -> a | _ -> failwith "" - with Failure _ -> errorlabstrm "elimination_clause" + with Failure _ -> user_err "elimination_clause" (str "The type of elimination clause is not well-formed.") in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in let hyp = mkVar id in @@ -1534,7 +1534,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in if Term.eq_constr hyp_typ new_hyp_typ then - errorlabstrm "general_rewrite_in" + user_err "general_rewrite_in" (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) @@ -2015,7 +2015,7 @@ let clear_body ids = let map = function | LocalAssum (id,t) as decl -> let () = if List.mem_f Id.equal id ids then - errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition") + user_err "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition") in decl | LocalDef (id,_,t) as decl -> @@ -2146,7 +2146,7 @@ let check_number_of_constructors expctdnumopt i nconstr = if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when not (Int.equal n nconstr) -> - errorlabstrm "Tactics.check_number_of_constructors" + user_err "Tactics.check_number_of_constructors" (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".") | _ -> () end; @@ -2725,7 +2725,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t let generalized_name c t ids cl = function | Name id as na -> if Id.List.mem id ids then - errorlabstrm "" (pr_id id ++ str " is already used."); + user_err "" (pr_id id ++ str " is already used."); na | Anonymous -> match kind_of_term c with @@ -2886,7 +2886,7 @@ let specialize (c,lbind) ipat = let tstack = chk tstack in let term = applist(thd,List.map (nf_evar clause.evd) tstack) in if occur_meta term then - errorlabstrm "" (str "Cannot infer an instance for " ++ + user_err "" (str "Cannot infer an instance for " ++ pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ str "."); @@ -2931,7 +2931,7 @@ let unfold_body x = (** We normalize the given hypothesis immediately. *) let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let xval = match Context.Named.lookup x hyps with - | LocalAssum _ -> errorlabstrm "unfold_body" + | LocalAssum _ -> user_err "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") | LocalDef (_,xval,_) -> xval in @@ -3428,7 +3428,7 @@ let make_up_names n ind_opt cname = let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in - errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") + user_err "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") let glob = Universes.constr_of_global @@ -4046,7 +4046,7 @@ let recolle_clenv i params args elimclause gl = (fun x -> match kind_of_term x with | Meta mv -> mv - | _ -> errorlabstrm "elimination_clause" + | _ -> user_err "elimination_clause" (str "The type of the elimination clause is not well-formed.")) arr in let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in @@ -4193,7 +4193,7 @@ let clear_unselected_context id inhyps cls = let open Context.Named.Declaration in if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences - then errorlabstrm "" + then user_err "" (str "Conclusion must be mentioned: it depends on " ++ pr_id id ++ str "."); match cls.onhyps with diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 180b836ea..d6c2ccad2 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -340,7 +340,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i mkVar seq) list_id )) and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff - with Not_found -> errorlabstrm "AutoIndDecl.eqI" + with Not_found -> user_err "AutoIndDecl.eqI" (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed."); in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff @@ -633,7 +633,7 @@ let side_effect_of_mode = function let make_bl_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then - errorlabstrm "" + user_err "" (str "Automatic building of boolean->Leibniz lemmas not supported"); let ind = (mind,0) in let nparams = mib.mind_nparams in @@ -756,7 +756,7 @@ let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") let make_lb_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then - errorlabstrm "" + user_err "" (str "Automatic building of Leibniz->boolean lemmas not supported"); let ind = (mind,0) in let nparams = mib.mind_nparams in diff --git a/toplevel/class.ml b/toplevel/class.ml index 6d53ec9d8..bf17867e8 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -98,7 +98,7 @@ let class_of_global = function | IndRef sp -> CL_IND sp | VarRef id -> CL_SECVAR id | ConstructRef _ as c -> - errorlabstrm "class_of_global" + user_err "class_of_global" (str "Constructors, such as " ++ Printer.pr_global c ++ str ", cannot be used as a class.") @@ -177,7 +177,7 @@ let ident_key_of_class = function (* Identity coercion *) let error_not_transparent source = - errorlabstrm "build_id_coercion" + user_err "build_id_coercion" (pr_class source ++ str " must be a transparent constant.") let build_id_coercion idf_opt source poly = @@ -208,7 +208,7 @@ let build_id_coercion idf_opt source poly = (Reductionops.is_conv_leq env sigma (Typing.unsafe_type_of env sigma val_f) typ_f) then - errorlabstrm "" (strbrk + user_err "" (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") in let idf = @@ -284,7 +284,7 @@ let add_new_coercion_core coef stre poly source target isid = let try_add_new_coercion_core ref ~local c d e f = try add_new_coercion_core ref (loc_of_bool local) c d e f with CoercionError e -> - errorlabstrm "try_add_new_coercion_core" + user_err "try_add_new_coercion_core" (explain_coercion_error ref e ++ str ".") let try_add_new_coercion ref ~local poly = diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 26cb7451a..6d62ce24a 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -169,7 +169,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p Name id -> let sp = Lib.make_path id in if Nametab.exists_cci sp then - errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists."); + user_err "new_instance" (Nameops.pr_id id ++ Pp.str " already exists."); id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in diff --git a/toplevel/command.ml b/toplevel/command.ml index b9a72fa33..4d333c30d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l = match n with | Some n -> mkIdentC (snd n) | None -> - errorlabstrm "do_program_fixpoint" + user_err "do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn @@ -1326,7 +1326,7 @@ let do_program_fixpoint local poly l = do_program_recursive local poly fixkind fixl ntns | _, _ -> - errorlabstrm "do_program_fixpoint" + user_err "do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") let check_safe () = diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index d9cd574a0..b90e62048 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -136,7 +136,7 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - CErrors.errorlabstrm "get_compat_version" + CErrors.user_err "get_compat_version" (str "Compatibility with version " ++ str s ++ str " not supported.") - | s -> CErrors.errorlabstrm "get_compat_version" + | s -> CErrors.user_err "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".") diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 6d57a21dc..fee5cffeb 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -87,7 +87,7 @@ let declare_scheme_object s aux f = try let _ = Hashtbl.find scheme_object_table key in (* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) - errorlabstrm "IndTables.declare_scheme_object" + user_err "IndTables.declare_scheme_object" (str "Scheme object " ++ str key ++ str " already declared.") with Not_found -> Hashtbl.add scheme_object_table key (s,f); diff --git a/toplevel/locality.ml b/toplevel/locality.ml index 154f787ef..7664acbb6 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 - CErrors.errorlabstrm "Locality.check_locality" + CErrors.user_err "Locality.check_locality" (str "This command does not support the \"" ++ str s ++ str "\" prefix.") | None -> () diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a1edb7139..cef074699 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -238,7 +238,7 @@ let rec find_pattern nt xl = function | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | _, Terminal s :: _ | Terminal s :: _, _ -> - errorlabstrm "Metasyntax.find_pattern" + user_err "Metasyntax.find_pattern" (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") | _, [] -> error msg_expected_form_of_recursive_notation @@ -300,7 +300,7 @@ let rec get_notation_vars = function let vars = get_notation_vars sl in if Id.equal id ldots_var then vars else if Id.List.mem id vars then - errorlabstrm "Metasyntax.get_notation_vars" + user_err "Metasyntax.get_notation_vars" (str "Variable " ++ pr_id id ++ str " occurs more than once.") else id::vars @@ -314,7 +314,7 @@ let analyze_notation_tokens l = recvars, List.subtract Id.equal vars (List.map snd recvars), l let error_not_same_scope x y = - errorlabstrm "Metasyntax.error_not_name_scope" + user_err "Metasyntax.error_not_name_scope" (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.") (**********************************************************************) @@ -390,7 +390,7 @@ let check_open_binder isopen sl m = | _ -> assert false in if isopen && not (List.is_empty sl) then - errorlabstrm "" (str "as " ++ pr_id m ++ + user_err "" (str "as " ++ pr_id m ++ str " is a non-closed binder, no such \"" ++ prlist_with_sep spc pr_token sl ++ strbrk "\" is allowed to occur.") @@ -661,7 +661,7 @@ let pr_level ntn (from,args) = prlist_with_sep pr_comma (pr_arg_level from) args let error_incompatible_level ntn oldprec prec = - errorlabstrm "" + user_err "" (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ @@ -731,7 +731,7 @@ let interp_modifiers modl = | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then - errorlabstrm "Metasyntax.interp_modifiers" + user_err "Metasyntax.interp_modifiers" (str s ++ str " is already assigned to an entry or constr level."); interp assoc level ((id,typ)::etyps) format extra l | SetItemLevel ([],n) :: l -> @@ -739,7 +739,7 @@ let interp_modifiers modl = | SetItemLevel (s::idl,n) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then - errorlabstrm "Metasyntax.interp_modifiers" + user_err "Metasyntax.interp_modifiers" (str s ++ str " is already assigned to an entry or constr level."); let typ = ETConstr (n,()) in interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l) @@ -770,7 +770,7 @@ let check_infix_modifiers modifiers = let check_useless_entry_types recvars mainvars etyps = let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with - | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types" + | (x,_)::_ -> user_err "Metasyntax.check_useless_entry_types" (pr_id x ++ str " is unbound in the notation.") | _ -> () @@ -813,7 +813,7 @@ let join_auxiliary_recursive_types recvars etyps = | None, Some ytyp -> (x,ytyp)::typs | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *) | Some xtyp, Some ytyp -> - errorlabstrm "" + user_err "" (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++ strbrk ", both ends have incompatible types.")) recvars etyps diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index fbd1e6033..c74c3522d 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -124,13 +124,13 @@ let ml_load s = | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e) | exc -> let msg = report_on_load_obj_error exc in - errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ + user_err "Mltop.load_object" (str"Cannot link ml-object " ++ str s ++ str" to Coq code (" ++ msg ++ str ").")) | WithoutTop -> try Dynlink.loadfile s; s with Dynlink.Error a -> - errorlabstrm "Mltop.load_object" + user_err "Mltop.load_object" (strbrk "while loading " ++ str s ++ strbrk ": " ++ str (Dynlink.error_message a)) @@ -151,7 +151,7 @@ let dir_ml_use s = if Dynlink.is_native then " Loading ML code works only in bytecode." else "" in - errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) + user_err "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) (* Adds a path to the ML paths *) let add_ml_dir s = @@ -221,7 +221,7 @@ let get_ml_object_suffix name = let file_of_name name = let suffix = get_ml_object_suffix name in let fail s = - errorlabstrm "Mltop.load_object" + user_err "Mltop.load_object" (str"File not found on loadpath : " ++ str s ++ str"\n" ++ str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in if not (Filename.is_relative name) then @@ -355,7 +355,7 @@ let trigger_ml_object verb cache reinit ?path name = add_loaded_module name (known_module_path name); if cache then perform_cache_obj name end else if not has_dynlink then - errorlabstrm "Mltop.trigger_ml_object" + user_err "Mltop.trigger_ml_object" (str "Dynamic link not supported (module " ++ str name ++ str ")") else begin let file = file_of_name (Option.default name path) in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 38d4a62b4..b9fd2894d 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -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 = CErrors.errorlabstrm "Program" cmd +let pperror cmd = CErrors.user_err "Program" cmd let error s = pperror (str s) let reduce c = @@ -398,7 +398,7 @@ let rec prod_app t n = | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> - errorlabstrm "prod_app" + user_err "prod_app" (str"Needed a product, but didn't find one" ++ fnl ()) @@ -444,7 +444,7 @@ let from_prg : program_info ProgMap.t ref = let close sec = if not (ProgMap.is_empty !from_prg) then let keys = map_keys !from_prg in - errorlabstrm "Program" + user_err "Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ @@ -718,7 +718,7 @@ let get_prog name = let progs = Id.Set.elements (ProgMap.domain prg_infos) in let prog = List.hd progs in let progs = prlist_with_sep pr_comma Nameops.pr_id progs in - errorlabstrm "" + user_err "" (str "More than one program with unsolved obligations: " ++ progs ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\"")) diff --git a/toplevel/record.ml b/toplevel/record.ml index 6a64b0d66..22dc8c957 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -208,7 +208,7 @@ let warning_or_error coe indsp err = | _ -> (pr_id fi ++ strbrk " cannot be defined because it is not typable.") in - if coe then errorlabstrm "structure" st; + if coe then user_err "structure" st; Flags.if_verbose Feedback.msg_info (hov 0 st) type field_status = @@ -235,7 +235,7 @@ let subst_projection fid l c = | Projection t -> lift depth t | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k | NoProjection Anonymous -> - errorlabstrm "" (str "Field " ++ pr_id fid ++ + user_err "" (str "Field " ++ pr_id fid ++ str " depends on the " ++ pr_nth (k-depth-1) ++ str " field which has no name.") else diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3f784fd8a..9e3494145 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -483,7 +483,7 @@ let vernac_start_proof locality p kind l lettop = | None -> ()) l; if not(refining ()) then if lettop then - errorlabstrm "Vernacentries.StartProof" + user_err "Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); start_proof_and_print (local, p, Proof kind) l no_hook @@ -855,7 +855,7 @@ let vernac_set_used_variables e = let vars = Environ.named_context env in List.iter (fun id -> if not (List.exists (Id.equal id % get_id) vars) then - errorlabstrm "vernac_set_used_variables" + user_err "vernac_set_used_variables" (str "Unknown variable: " ++ pr_id id)) l; let _, to_clear = set_used_variables l in @@ -974,9 +974,9 @@ let vernac_declare_arguments locality r l nargs flags = | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls | [], _::_, (Some _)::ls when extra_scope_flag -> error "Extra notation scopes can be set on anonymous arguments only" - | [], x::_, _ -> errorlabstrm "vernac_declare_arguments" + | [], x::_, _ -> user_err "vernac_declare_arguments" (str "Extra argument " ++ pr_name x ++ str ".") - | l, [], _ -> errorlabstrm "vernac_declare_arguments" + | l, [], _ -> user_err "vernac_declare_arguments" (str "The following arguments are not declared: " ++ prlist_with_sep pr_comma pr_name l ++ str ".") | _::li, _::ld, _::ls -> check li ld ls @@ -1019,7 +1019,7 @@ let vernac_declare_arguments locality r l nargs flags = let sr', impl = List.fold_map (fun b -> function | (Anonymous, _,_, true, max), Name id -> assert false | (Name x, _,_, true, _), Anonymous -> - errorlabstrm "vernac_declare_arguments" + user_err "vernac_declare_arguments" (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> set_renamed iid id; @@ -1033,7 +1033,7 @@ let vernac_declare_arguments locality r l nargs flags = some_renaming_specified l in if some_renaming_specified then if not (List.mem `Rename flags) then - errorlabstrm "vernac_declare_arguments" + user_err "vernac_declare_arguments" (str "To rename arguments the \"rename\" flag must be specified." ++ match !renamed_arg with | None -> mt () @@ -1077,7 +1077,7 @@ let vernac_declare_arguments locality r l nargs flags = | ConstRef _ as c -> Reductionops.ReductionBehaviour.set (make_section_locality locality) c (rargs, nargs, flags) - | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") + | _ -> user_err "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") end; if not (some_renaming_specified || some_implicits_specified || @@ -1498,7 +1498,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) (try get_nth_goal n,id with - Failure _ -> errorlabstrm "print_about_hyp_globs" + Failure _ -> user_err "print_about_hyp_globs" (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in @@ -1597,7 +1597,7 @@ let interp_search_about_item env = (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> - errorlabstrm "interp_search_about_item" + user_err "interp_search_about_item" (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") let vernac_search s gopt r = @@ -1877,12 +1877,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 -> 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") + | VernacAbort id -> CErrors.user_err "" (str "Abort cannot be used through the Load command") + | VernacAbortAll -> CErrors.user_err "" (str "AbortAll cannot be used through the Load command") + | VernacRestart -> CErrors.user_err "" (str "Restart cannot be used through the Load command") + | VernacUndo _ -> CErrors.user_err "" (str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> CErrors.user_err "" (str "UndoTo cannot be used through the Load command") + | VernacBacktrack _ -> CErrors.user_err "" (str "Backtrack cannot be used through the Load command") (* Proof management *) | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false @@ -2014,7 +2014,7 @@ let with_fail b f = let (e, _) = CErrors.push e in match e with | HasNotFailed -> - errorlabstrm "Fail" (str "The command has not failed!") + user_err "Fail" (str "The command has not failed!") | HasFailed msg -> if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index d81e3d6b5..147727e7c 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -22,7 +22,7 @@ let vinterp_add depr s f = try Hashtbl.add vernac_tab s (depr, f) with Failure _ -> - errorlabstrm "vinterp_add" + user_err "vinterp_add" (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") let overwriting_vinterp_add s f = @@ -37,7 +37,7 @@ let vinterp_map s = try Hashtbl.find vernac_tab s with Failure _ | Not_found -> - errorlabstrm "Vernac Interpreter" + user_err "Vernac Interpreter" (str"Cannot find vernac command " ++ str (fst s) ++ str".") let vinterp_init () = Hashtbl.clear vernac_tab -- cgit v1.2.3