From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

---
 tactics/contradiction.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics/contradiction.ml')

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index afc7e1547..a3a448aad 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -116,7 +116,6 @@ let contradiction_term (c,lbind as cl) =
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let typ = type_of c in
-    let typ = EConstr.of_constr typ in
     let _, ccl = splay_prod env sigma typ in
     if is_empty_type sigma ccl then
       Tacticals.New.tclTHEN
-- 
cgit v1.2.3