diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/logic_monad.ml | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 17ff898b0f..e14a2bd396 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 576569cf5f..c47c44e222 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 |