diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 855235d2b0..333ae78b3a 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -341,7 +341,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 @@ -427,7 +427,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 @@ -839,11 +839,11 @@ let tclPROGRESS t = if not test then tclUNIT res else - tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") | _ -> Pervasives.raise CErrors.Unhandled end @@ -1050,7 +1050,7 @@ module Goal = struct exception NotExactlyOneSubgoal let _ = CErrors.register_handler begin function | NotExactlyOneSubgoal -> - CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.") + CErrors.user_err (Pp.str"Not exactly one subgoal.") | _ -> raise CErrors.Unhandled end |