diff options
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 445a104d6..6b29f574c 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -13,7 +13,8 @@ open Coqlib open Reductionops open Misctypes open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* Absurd *) @@ -48,7 +49,7 @@ let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 let filter_hyp f tac = let rec seek = function | [] -> Proofview.tclZERO Not_found - | d::rest when f (get_type d) -> tac (get_id d) + | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in @@ -62,8 +63,8 @@ let contradiction_context = let rec seek_neg l = match l with | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> - let id = get_id d in - let typ = nf_evar sigma (get_type d) in + let id = NamedDecl.get_id d in + let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in if is_empty_type typ then simplest_elim (mkVar id) |