diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 55 |
1 files changed, 27 insertions, 28 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 10bbdc358..6e632999c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -385,9 +385,9 @@ let err_unmapped_library loc ?from qid = | Some from -> str " and prefix " ++ pr_dirpath from ++ str "." in - user_err_loc - (loc,"locate_library", - strbrk "Cannot find a physical path bound to logical path matching suffix " ++ + user_err ~loc + ~hdr:"locate_library" + (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ pr_dirpath dir ++ prefix) let err_notfound_library loc ?from qid = @@ -396,9 +396,8 @@ let err_notfound_library loc ?from qid = | Some from -> str " with prefix " ++ pr_dirpath from ++ str "." in - user_err_loc - (loc,"locate_library", - strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) + user_err ~loc ~hdr:"locate_library" + (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = let (loc,qid) = qualid_of_reference r in @@ -489,7 +488,7 @@ let vernac_start_proof locality p kind l lettop = | None -> ()) l; if not(refining ()) then if lettop then - errorlabstrm "Vernacentries.StartProof" + user_err ~hdr:"Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); start_proof_and_print (local, p, Proof kind) l no_hook @@ -610,15 +609,15 @@ let vernac_combined_scheme lid l = let vernac_universe loc poly l = if poly && not (Lib.sections_are_opened ()) then - user_err_loc (loc, "vernac_universe", - str"Polymorphic universes can only be declared inside sections, " ++ + user_err ~loc ~hdr:"vernac_universe" + (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); do_universe poly l let vernac_constraint loc poly l = if poly && not (Lib.sections_are_opened ()) then - user_err_loc (loc, "vernac_constraint", - str"Polymorphic universe constraints can only be declared" + user_err ~loc ~hdr:"vernac_constraint" + (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); do_constraint poly l @@ -860,7 +859,7 @@ let vernac_set_used_variables e = let vars = Environ.named_context env in List.iter (fun id -> if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then - errorlabstrm "vernac_set_used_variables" + user_err ~hdr:"vernac_set_used_variables" (str "Unknown variable: " ++ pr_id id)) l; let _, to_clear = set_used_variables l in @@ -979,9 +978,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 ~hdr:"vernac_declare_arguments" (str "Extra argument " ++ pr_name x ++ str ".") - | l, [], _ -> errorlabstrm "vernac_declare_arguments" + | l, [], _ -> user_err ~hdr:"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 @@ -1024,7 +1023,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 ~hdr:"vernac_declare_arguments" (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> set_renamed iid id; @@ -1038,7 +1037,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 ~hdr:"vernac_declare_arguments" (str "To rename arguments the \"rename\" flag must be specified." ++ match !renamed_arg with | None -> mt () @@ -1082,7 +1081,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 || @@ -1503,7 +1502,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 ~hdr:"print_about_hyp_globs" (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in @@ -1579,8 +1578,8 @@ let global_module r = let (loc,qid) = qualid_of_reference r in try Nametab.full_name_module qid with Not_found -> - user_err_loc (loc, "global_module", - str "Module/section " ++ pr_qualid qid ++ str " not found.") + user_err ~loc ~hdr:"global_module" + (str "Module/section " ++ pr_qualid qid ++ str " not found.") let interp_search_restriction = function | SearchOutside l -> (List.map global_module l, true) @@ -1602,7 +1601,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 ~hdr:"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 = @@ -1882,12 +1881,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 @@ -2019,7 +2018,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 ~hdr:"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) |