diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-03-09 15:15:38 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-03-09 16:23:05 +0100 |
| commit | a5ae3b2856e6cc6683652a0abb5a84b9787527c0 (patch) | |
| tree | dc9cccac803a02f1c2e45cfa87a67a95dee0c538 /test-suite/success/keyedrewrite.v | |
| parent | d34a2ff176c75ea404f7eb638b6eea3ca07ab978 (diff) | |
Fix strategy of Keyed Unification
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
Diffstat (limited to 'test-suite/success/keyedrewrite.v')
| -rw-r--r-- | test-suite/success/keyedrewrite.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index 5b0502cf1..b88c142be 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -58,4 +58,5 @@ Qed. Lemma test b : b && true = b. Fail rewrite andb_true_l. - Admitted.
\ No newline at end of file + Admitted. +
\ No newline at end of file |