From fc642ca962dd5228a5a714b8e41506dcbc3b6520 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 12 Jan 2016 19:27:02 +0100
Subject: Extend last commit: keyed unification uses full conversions on the
 applied constant and arguments _separately_.

---
 test-suite/success/keyedrewrite.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

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
-- 
cgit v1.2.3