diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r-- | toplevel/vernacentries.ml | 32 |
1 files changed, 16 insertions, 16 deletions
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) |