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 | |
| 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.
| -rw-r--r-- | pretyping/unification.ml | 10 | ||||
| -rw-r--r-- | printing/pptactic.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 3 |
3 files changed, 11 insertions, 4 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. diff --git a/printing/pptactic.ml b/printing/pptactic.ml index e6157793e3..785b0e8dce 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -581,7 +581,7 @@ let make_pr_tac pr_tac_level pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,pr_alias,strip_prod_binders, pr_gen) = (* some shortcuts *) -let pr_bindings = pr_bindings pr_constr pr_lconstr in +let _pr_bindings = pr_bindings pr_constr pr_lconstr in let pr_ex_bindings = pr_bindings_gen true pr_constr pr_lconstr in let pr_with_bindings = pr_with_bindings pr_constr pr_lconstr in let pr_with_bindings_arg = pr_with_bindings_arg pr_constr pr_lconstr in 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 |