diff options
| -rw-r--r-- | engine/proofview.ml | 18 | ||||
| -rw-r--r-- | proofs/proof.ml | 15 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 7 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 2 |
5 files changed, 19 insertions, 25 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 16be96454e..b0ea75ac60 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -302,7 +302,8 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") + | MoreThanOneSuccess -> + Pp.str "This tactic has more than one success." | _ -> raise CErrors.Unhandled end @@ -347,8 +348,7 @@ exception NoSuchGoals of int let _ = CErrors.register_handler begin function | NoSuchGoals n -> - CErrors.user_err - (str "No such " ++ str (String.plural n "goal") ++ str ".") + str "No such " ++ str (String.plural n "goal") ++ str "." | _ -> raise CErrors.Unhandled end @@ -420,12 +420,9 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function | SizeMismatch (i,j) -> - let open Pp in - let errmsg = - str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." - in - CErrors.user_err errmsg + let open Pp in + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." | _ -> raise CErrors.Unhandled end @@ -910,7 +907,8 @@ let tclPROGRESS t = tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) let _ = CErrors.register_handler begin function - | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Logic_monad.Tac_Timeout -> + Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!" | _ -> raise CErrors.Unhandled end diff --git a/proofs/proof.ml b/proofs/proof.ml index 5ab4409f8b..e2ee5426b5 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -69,18 +69,15 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") + Pp.str "This proof is focused, but cannot be unfocused this way" | NoSuchGoals (i,j) when Int.equal i j -> - CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") + Pp.(str "[Focus] No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - CErrors.user_err ~hdr:"Focus" Pp.( - str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." - ) + Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") | NoSuchGoal id -> - CErrors.user_err - ~hdr:"Focus" - Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".") - | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") + Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") + | FullyUnfocused -> + Pp.str "The proof is not focused" | _ -> raise CErrors.Unhandled end diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 66e2ae5c29..61e8741973 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -79,7 +79,7 @@ module Strict = struct (function | FailedBullet (b,sugg) -> let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in - CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg) + Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) | _ -> raise CErrors.Unhandled) @@ -204,8 +204,7 @@ exception SuggestNoSuchGoals of int * Proof.t let _ = CErrors.register_handler begin function | SuggestNoSuchGoals(n,proof) -> let suffix = suggest proof in - CErrors.user_err - Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ - pr_non_empty_arg (fun x -> x) suffix) + Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix) | _ -> raise CErrors.Unhandled end diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 3c9803432a..a4a06873b8 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -27,7 +27,7 @@ let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal let () = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") + | NoSuchGoal -> Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index c81a4abc1b..80b72225f0 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -124,7 +124,7 @@ module Proof_global = struct let () = CErrors.register_handler begin function | NoCurrentProof -> - CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") + Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end |