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.

1 files changed, 8 insertions, 2 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e6a34929d4..f04a7294f1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1334,11 +1334,15 @@ let make_abstraction env evd ccl abs =
    Unifies [cl] to every subterm of [op] until it finds a match.
    Fails if no match is found *)
 let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
+  let bestexn = ref None in
   let rec matchrec cl =
     let cl = strip_outer_cast cl in
     (try
        if closed0 cl && not (isEvar cl)
-       then w_typed_unify env evd CONV flags op cl,cl
+       then
+	 (try w_typed_unify env evd CONV flags op cl,cl
+	  with ex when Typeclasses_errors.unsatisfiable_exception ex ->
+	    bestexn := Some ex; error "Unsat")
        else error "Bound 1"
      with ex when precatchable_exception ex ->
        (match kind_of_term cl with
@@ -1390,7 +1394,9 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
-    raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
+    match !bestexn with
+    | None -> raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
+    | Some e -> raise e
 
 (* Tries to find all instances of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] and return all the matches.