diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-01-12 19:27:02 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-01-12 19:27:02 +0100 |
| commit | fc642ca962dd5228a5a714b8e41506dcbc3b6520 (patch) | |
| tree | 12903d09cdc87b6d3964d0a9e7b27e49d5413c57 /test-suite/success/keyedrewrite.v | |
| parent | eb40037b4c341746933c713e8950f3a60d550f4a (diff) | |
Extend last commit: keyed unification uses full conversions on the applied constant and arguments _separately_.
Diffstat (limited to 'test-suite/success/keyedrewrite.v')
| -rw-r--r-- | test-suite/success/keyedrewrite.v | 6 |
1 files changed, 6 insertions, 0 deletions
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 |