diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-08-14 15:56:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-08-14 16:02:02 +0200 |
| commit | c69404402212ed9d541899ae78ac889e62cf238a (patch) | |
| tree | 11f313c9b5ddb0c61c2250cf305fe9d6e717a008 /pretyping | |
| 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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 2 insertions, 4 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 = |