diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
| commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
| tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /tactics/contradiction.ml | |
| parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) | |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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 |