diff options
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 565f30cfb..ed1661910 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -44,12 +44,12 @@ let filter_hyp f tac = | [] -> raise Not_found | (id,_,t)::rest when f t -> tac id | _::rest -> seek rest in - Goal.hyps >>- fun hyps -> + Proofview.Goal.hyps >>- fun hyps -> seek (Environ.named_context_of_val hyps) let contradiction_context = - Goal.env >>- fun env -> - Goal.defs >>- fun sigma -> + Proofview.tclEVARMAP >= fun sigma -> + Proofview.Goal.env >>- fun env -> let rec seek_neg l = match l with | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction")) | (id,_,typ)::rest -> @@ -69,7 +69,7 @@ let contradiction_context = | e -> Proofview.tclZERO e end) | _ -> seek_neg rest in - Goal.hyps >>- fun hyps -> + Proofview.Goal.hyps >>- fun hyps -> let hyps = Environ.named_context_of_val hyps in seek_neg hyps @@ -79,8 +79,8 @@ let is_negation_of env sigma typ t = | _ -> false let contradiction_term (c,lbind as cl) = - Goal.env >>- fun env -> - Goal.defs >>- fun sigma -> + Proofview.tclEVARMAP >= fun sigma -> + Proofview.Goal.env >>- fun env -> Tacmach.New.pf_apply Typing.type_of >>- fun type_of -> let typ = type_of c in let _, ccl = splay_prod env sigma typ in |