1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/success/setoid_unif.v b/test-suite/success/setoid_unif.v
new file mode 100644
index 00000000..912596b4
--- /dev/null
+++ b/test-suite/success/setoid_unif.v
@@ -0,0 +1,27 @@
+(* An example of unification in rewrite which uses eager substitution
+   of metas (provided by Pierre-Marie).
+
+   Put in the test suite as an indication of what the use metas
+   eagerly flag provides, even though the concrete cases that use it
+   are seldom. Today supported thanks to a new flag for using evars
+   eagerly, after this variant of setoid rewrite started to use clause
+   environments based on evars (fbbe491cfa157da627) *)
+
+Require Import Setoid.
+
+Parameter elt : Type.
+Parameter T : Type -> Type.
+Parameter empty : forall A, T A.
+Parameter MapsTo : forall A : Type, elt -> A -> T A -> Prop.
+
+(* Definition In A x t := exists e, MapsTo A x e t. *)
+Axiom In : forall A, A -> T A -> Prop.
+Axiom foo : forall A x, In A x (empty A) <-> False.
+
+Record R := { t : T unit; s : unit }.
+Definition Empty := {| t := empty unit; s := tt |}.
+
+Goal forall x, ~ In _ x (t Empty).
+Proof.
+intros x.
+rewrite foo.