Imported Upstream version 8.5~beta1+dfsg

1 files changed, 24 insertions, 0 deletions

diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
new file mode 100644
index 00000000..bbe9d4bf
--- /dev/null
+++ b/test-suite/success/keyedrewrite.v
@@ -0,0 +1,24 @@
+Set Keyed Unification.
+
+Section foo.
+Variable f : nat -> nat. 
+
+Definition g := f.
+
+Variable lem : g 0 = 0.
+
+Goal f 0 = 0.
+Proof.
+  Fail rewrite lem.
+Abort.
+
+Declare Equivalent Keys @g @f.
+(** Now f and g are considered equivalent heads for subterm selection *)
+Goal f 0 = 0.
+Proof.
+  rewrite lem.
+  reflexivity.
+Qed.
+
+Print Equivalent Keys.
+End foo.