diff options
Diffstat (limited to 'test-suite/success')
| -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 |