Fix bug #4679, weakened setoid_rewrite unification

It should use evar instantiations eagerly during unification of
the lhs of the lemma, as in 8.4.

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v
new file mode 100644
index 000000000..c94fa31a9
--- /dev/null
+++ b/test-suite/bugs/closed/4679.v
@@ -0,0 +1,18 @@
+Require Import Coq.Setoids.Setoid.
+Goal forall (T : nat -> Set -> Set) (U : Set)
+            (H : forall n : nat, T n (match n with
+                                      | 0 => fun x => x
+                                      | S _ => fun x => x
+                                      end (nat = nat)) = U),
+    T 0 (nat = nat) = U.
+Proof.
+  intros.
+  let H := match goal with H : forall _, eq _ _ |- _ => H end in
+  rewrite H || fail 0 "too early".
+  Undo.
+  let H := match goal with H : forall _, eq _ _ |- _ => H end in
+  setoid_rewrite (H 0) || fail 0 "too early".
+  Undo.
+  setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *)
+  reflexivity.
+Qed.
\ No newline at end of file