Extend Keyed Unification tests with the one from R. Krebbers.

1 files changed, 31 insertions, 0 deletions

diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index bbe9d4bff..d1a93581c 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -22,3 +22,34 @@ Qed.
 
 Print Equivalent Keys.
 End foo.
+
+Require Import Arith List Omega.
+
+Definition G {A} (f : A -> A -> A) (x : A) := f x x.
+
+Lemma list_foo A (l : list A) : G (@app A) (l ++ nil) = G (@app A) l.
+Proof. unfold G; rewrite app_nil_r; reflexivity. Qed.
+
+(* Bundled version of a magma *)
+Structure magma := Magma { b_car :> Type; op : b_car -> b_car -> b_car }.
+Arguments op {_} _ _.
+
+(* Instance for lists *)
+Canonical Structure list_magma A := Magma (list A) (@app A).
+
+(* Basically like list_foo, but now uses the op projection instead of app for
+the argument of G *)
+Lemma test1 A (l : list A) : G op (l ++ nil) = G op l.
+
+(* Ensure that conversion of terms with evars is allowed once a keyed candidate unifier is found *)
+rewrite -> list_foo.
+reflexivity.
+Qed.
+
+(* Basically like list_foo, but now uses the op projection for everything *)
+Lemma test2 A (l : list A) : G op (op l nil) = G op l.
+Proof.
+rewrite ->list_foo.
+reflexivity.
+Qed.
+