diff options
Diffstat (limited to 'tactics/contradiction.ml')
-rw-r--r-- | tactics/contradiction.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9b69481d..22f218b4 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -55,7 +55,7 @@ let contradiction_context = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let rec seek_neg l = match l with - | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction")) + | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | (id,_,typ)::rest -> let typ = nf_evar sigma typ in let typ = whd_betadeltaiota env sigma typ in @@ -90,7 +90,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.nf_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then @@ -107,7 +107,7 @@ let contradiction_term (c,lbind as cl) = Proofview.tclZERO Not_found end begin function (e, info) -> match e with - | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction.")) + | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.") | e -> Proofview.tclZERO ~info e end end |