Follow up to experimental eager evar unification in bcba6d1bc9:

Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).

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 0000000000..912596b4a3
--- /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.