aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/contradiction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/contradiction.ml')
-rw-r--r--tactics/contradiction.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 19e5906f8..0198fc3fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -91,7 +91,7 @@ let contradiction_term (c,lbind as cl) =
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) (Proofview.V82.tactic (tclTRY assumption))
+ Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
else
Proofview.tclORELSE
begin