diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index c01879765..53cb77b95 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -22,6 +22,8 @@ open Context.Named.Declaration (** Main state of tactics *) type proofview = Proofview_monad.proofview +(* The first items in pairs below are proofs (under construction). + The second items in the pairs below are statements that are being proved. *) type entry = (Term.constr * Term.types) list (** Returns a stylised view of a proofview for use by, for instance, @@ -341,7 +343,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 +429,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 +841,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 +1052,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 |