diff options
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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 |