diff options
Diffstat (limited to 'tactics/contradiction.ml')
-rw-r--r-- | tactics/contradiction.ml | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9c8412454..f245247a9 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -90,25 +90,23 @@ let contradiction_term (c,lbind as cl) = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_type_of gl in - try (* type_of can raise exceptions. *) - let typ = type_of c in - let _, ccl = splay_prod env sigma typ in - if is_empty_type ccl then - Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption) - else - Proofview.tclORELSE - begin - if lbind = NoBindings then - filter_hyp (is_negation_of env sigma typ) - (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) - else - Proofview.tclZERO Not_found - end - begin function - | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction.")) - | e -> Proofview.tclZERO e - end - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + let typ = type_of c in + let _, ccl = splay_prod env sigma typ in + if is_empty_type ccl then + Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption) + else + Proofview.tclORELSE + begin + if lbind = NoBindings then + filter_hyp (is_negation_of env sigma typ) + (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) + else + Proofview.tclZERO Not_found + end + begin function + | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction.")) + | e -> Proofview.tclZERO e + end end let contradiction = function |