diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 18 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 10 |
2 files changed, 14 insertions, 14 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index e2ee5426b5..7d0b31734e 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -69,16 +69,16 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - Pp.str "This proof is focused, but cannot be unfocused this way" + Some (Pp.str "This proof is focused, but cannot be unfocused this way") | NoSuchGoals (i,j) when Int.equal i j -> - Pp.(str "[Focus] No such goal (" ++ int i ++ str").") + Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") + Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") | NoSuchGoal id -> - Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") + Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") | FullyUnfocused -> - Pp.str "The proof is not focused" - | _ -> raise CErrors.Unhandled + Some (Pp.str "The proof is not focused") + | _ -> None end let check_cond_kind c k = @@ -325,9 +325,9 @@ exception OpenProof of Names.Id.t option * open_error_reason let _ = CErrors.register_handler begin function | OpenProof (pid, reason) -> let open Pp in - Option.cata (fun pid -> - str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason - | _ -> raise CErrors.Unhandled + Some (Option.cata (fun pid -> + str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason) + | _ -> None end let warn_remaining_shelved_goals = diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 3ff0533b6b..d978885d62 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -79,8 +79,8 @@ module Strict = struct (function | FailedBullet (b,sugg) -> let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in - Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) - | _ -> raise CErrors.Unhandled) + Some Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) + | _ -> None) (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) @@ -203,7 +203,7 @@ exception SuggestNoSuchGoals of int * Proof.t let _ = CErrors.register_handler begin function | SuggestNoSuchGoals(n,proof) -> let suffix = suggest proof in - Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ - pr_non_empty_arg (fun x -> x) suffix) - | _ -> raise CErrors.Unhandled + Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix)) + | _ -> None end |