diff options
| author | Pierre-Marie Pédrot | 2020-03-19 12:07:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-19 12:07:27 +0100 |
| commit | b69b87ce35b09b164929974b85b815d259185f18 (patch) | |
| tree | ff0a3cebda0c7a60728caa7b7eb4beb209e1bf37 /tactics/equality.ml | |
| parent | a1315d78a5b3c6095848298f03ca328380a7d453 (diff) | |
| parent | 812665445fd370842a1b8abf7cddbd33f3ddaa5c (diff) | |
Merge PR #11735: Deprecating catchable_exception
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 6e859d997b..49645d82a4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -563,7 +563,7 @@ let apply_special_clear_request clear_flag f = let (sigma, (c, bl)) = f env sigma in apply_clear_request clear_flag (use_clear_hyp_by_default ()) c with - e when catchable_exception e -> tclIDTAC + e when noncritical e -> tclIDTAC end type multi = @@ -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 = |