diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /tactics/contradiction.ml | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
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 |