From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 19 Nov 2016 01:07:35 +0100
Subject: Inv API using EConstr.

---
 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 596f1a759..2d5c28eba 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -119,7 +119,6 @@ let contradiction_term (c,lbind as cl) =
     let typ = type_of c in
     let typ = EConstr.of_constr typ in
     let _, ccl = splay_prod env sigma typ in
-    let ccl = EConstr.of_constr ccl in
     if is_empty_type sigma ccl then
       Tacticals.New.tclTHEN
         (elim false None cl None)
-- 
cgit v1.2.3