From b9485da2388e0fe2d634d3359c0504b8c253e554 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 21 Jul 2016 17:03:46 +0200
Subject: 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.
---
 ltac/rewrite.ml               |  2 +-
 test-suite/bugs/closed/4679.v | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4679.v

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 0556191be8..e327deda02 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -581,7 +581,7 @@ let general_rewrite_unif_flags () =
   let core_flags =
     { rewrite_core_unif_flags with
       Unification.modulo_conv_on_closed_terms = Some ts;
-      Unification.use_evars_eagerly_in_conv_on_closed_terms = false;
+      Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
       Unification.modulo_delta = ts;
       Unification.modulo_delta_types = ts;
       Unification.modulo_betaiota = true }
diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v
new file mode 100644
index 0000000000..c94fa31a9d
--- /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
-- 
cgit v1.2.3