diff options
| author | Matthieu Sozeau | 2014-08-14 15:56:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-14 16:02:02 +0200 |
| commit | c69404402212ed9d541899ae78ac889e62cf238a (patch) | |
| tree | 11f313c9b5ddb0c61c2250cf305fe9d6e717a008 | |
| parent | cd98815d0e1e57eed3e19eb9516a980b82c60a36 (diff) | |
Remove confusing behavior of unify_with_subterm that could fail with
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.
| -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 a864ccc462..e6a34929d4 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 10b78ba2b3..51678e1748 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 |