diff options
| author | Hugo Herbelin | 2020-03-02 21:15:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-13 07:37:25 +0100 |
| commit | 89a5abb0b8b453bdda8c9ebf33734c42c3a826db (patch) | |
| tree | dc96f080513504f8b9609a18034c456453659caf /tactics | |
| parent | cd4253ee5db24873ea131554c80650ed6d5dbd13 (diff) | |
Removing catchable_exception test in tclOR/tclORELSE.
Since tclOR/tclORELSE are not supposed to return critical exceptions,
we don't need to replace catchable_exception by noncritical.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 11 | ||||
| -rw-r--r-- | tactics/equality.ml | 3 |
2 files changed, 5 insertions, 9 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e3f2f18b44..f92d0603ca 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -234,9 +234,8 @@ let unify_resolve_refine poly flags gl clenv = match fst ie with | Evarconv.UnableToUnify _ -> Tacticals.New.tclZEROMSG (str "Unable to unify") - | e when CErrors.noncritical e -> - Tacticals.New.tclZEROMSG (str "Unexpected error") - | _ -> Exninfo.iraise ie) + | e -> + Tacticals.New.tclZEROMSG (str "Unexpected error")) (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. @@ -447,7 +446,7 @@ let cut_of_hints h = let catchable = function | Refiner.FailError _ -> true - | e -> Logic.catchable_exception e + | e -> Logic.catchable_exception e [@@ocaml.warning "-3"] let pr_depth l = let rec fmt elts = @@ -769,9 +768,7 @@ module Search = struct (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) (fun e' -> - if CErrors.noncritical (fst e') then - (pr_error e'; aux (merge_exceptions e e') tl) - else Exninfo.iraise e') + (pr_error e'; aux (merge_exceptions e e') tl)) and aux e = function | x :: xs -> onetac e x xs | [] -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 9804d4754d..fb39a856e9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1627,10 +1627,9 @@ let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with | Constr_matching.PatternMatchingFailure -> tclZEROMSG (str "Not a primitive equality here.") - | e when catchable_exception e -> + | e -> tclZEROMSG (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") - | e -> Proofview.tclZERO ~info e end let cutSubstClause l2r eqn cls = |