diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index a74fceb8f..4b43a9e69 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -633,7 +633,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 ~hdr:"Hints" (str "No such Hint database: " ++ str x ++ str ".") (**************************************************************************) (* Definition of the summary *) @@ -775,7 +775,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 ~hdr:"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.")); @@ -818,7 +818,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 ~hdr:"Hint" (pr_global ref ++ str" has " ++ int n ++ str" arguments while the mode declares " ++ int (Array.length m')) else m' @@ -1412,6 +1412,6 @@ let run_hint tac k = match !warn_hint with else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x) | `STRICT -> if is_imported tac then k tac.obj - else Proofview.tclZERO (UserError ("", (str "Tactic failure."))) + else Proofview.tclZERO (UserError (None, (str "Tactic failure."))) let repr_hint h = h.obj |