diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-23 14:22:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-23 14:54:29 +0200 |
| commit | 915c8f15965fe8e7ee9d02a663fd890ef80539ad (patch) | |
| tree | fb99ec9a2cbc7f4ee9a5f59656816fa3d34c6e3a /tactics/contradiction.ml | |
| parent | 0a2dfa5e5d17ccf58328432888dff345ef0bf5e6 (diff) | |
Using tclZEROMSG instead of tclZERO in several places.
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9b69481da..c03710e91 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 @@ -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 |