diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 10b78ba2b..51678e174 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1954,10 +1954,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = (Refiner.tclEVARS hypinfo.cl.evd) (cl_rewrite_clause_tac ~abs:(Some abs) strat cl)) gl with RewriteFailure e -> - let {c1=x; c2=y} = hypinfo in - raise (Pretype_errors.PretypeError - (pf_env gl,project gl, - Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl))) + tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl open Proofview.Notations |