diff options
| author | Matthieu Sozeau | 2014-08-18 16:44:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-18 17:10:00 +0200 |
| commit | 8d5238f09a6d7e0b8cb64a21d5d1410c519ff1ab (patch) | |
| tree | 6d689ecdb3a61b93f234c57e33b812b3d743742c /tactics | |
| parent | c61e5783458d4b9f2cd104bd027893f6bdc82ded (diff) | |
Refine patch for behavior of unify_to_subterm to allow backtracking on
unsatisfiable constraint failures but give sensible error messages if
an occurrence was found and only typeclass resolution failed.
Fixes MathClasses.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 51678e1748..8592cd33d8 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1902,7 +1902,8 @@ let unification_rewrite l2r c1 c2 cl car rel but env = ~flags:{ rewrite_unif_flags with Unification.resolve_evars = true } env cl.evd ((if l2r then c1 else c2),but) with - Pretype_errors.PretypeError _ -> + | ex when Pretype_errors.precatchable_exception ex || + Typeclasses_errors.unsatisfiable_exception ex -> (* ~flags:(true,true) to make Ring work (since it really exploits conversion) *) Unification.w_unify_to_subterm |