diff options
| author | Matthieu Sozeau | 2016-01-12 19:27:02 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-01-12 19:27:02 +0100 |
| commit | fc642ca962dd5228a5a714b8e41506dcbc3b6520 (patch) | |
| tree | 12903d09cdc87b6d3964d0a9e7b27e49d5413c57 | |
| parent | eb40037b4c341746933c713e8950f3a60d550f4a (diff) | |
Extend last commit: keyed unification uses full conversions on the applied constant and arguments _separately_.
| -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 510d5761b7..48638474a8 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 d1a93581ca..5b0502cf1a 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 |