diff options
| -rw-r--r-- | pretyping/unification.ml | 9 | ||||
| -rw-r--r-- | test-suite/success/keyedrewrite.v | 6 |
2 files changed, 13 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 510d5761b..48638474a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1649,8 +1649,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let cl = strip_outer_cast cl in (try if closed0 cl && not (isEvar cl) && keyed_unify env evd kop cl then - (try w_typed_unify env evd CONV flags op cl,cl - with ex when Pretype_errors.unsatisfiable_exception ex -> + (try + if !keyed_unification then + let f1, l1 = decompose_app_vect op in + let f2, l2 = decompose_app_vect cl in + w_typed_unify_array env evd flags f1 l1 f2 l2,cl + else w_typed_unify env evd CONV flags op cl,cl + with ex when Pretype_errors.unsatisfiable_exception ex -> bestexn := Some ex; error "Unsat") else error "Bound 1" with ex when precatchable_exception ex -> diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index d1a93581c..5b0502cf1 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -53,3 +53,9 @@ rewrite ->list_foo. reflexivity. Qed. + Require Import Bool. + Set Keyed Unification. + + Lemma test b : b && true = b. + Fail rewrite andb_true_l. + Admitted.
\ No newline at end of file |