diff options
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index b92bc75bc..e12063fd4 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -14,7 +14,6 @@ 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 |