diff options
| -rw-r--r-- | pretyping/unification.ml | 6 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 5 |
2 files changed, 3 insertions, 8 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a864ccc46..e6a34929d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1120,10 +1120,8 @@ let check_types env flags (sigma,_,_ as subst) m n = let try_resolve_typeclasses env evd flags m n = if flags.resolve_evars then - try Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false - ~fail:true env evd - with e when Typeclasses_errors.unsatisfiable_exception e -> - error_cannot_unify env evd (m, n) + Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false + ~fail:true env evd else evd let w_unify_core_0 env evd with_types cv_pb flags m n = 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 |