From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 tactics/contradiction.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics/contradiction.ml')

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c285f21e..e12063fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -8,13 +8,12 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Hipattern
 open Tactics
 open Coqlib
 open Reductionops
-open Misctypes
 open Proofview.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) =
     else
       Proofview.tclORELSE
         begin
-          if lbind = NoBindings then
+          if lbind = Tactypes.NoBindings then
             filter_hyp (fun c -> is_negation_of env sigma typ c)
               (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
           else
-- 
cgit v1.2.3