From 18489538b2fd1e576b0df3af274925b5b81c10e8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 18 Oct 2011 15:22:19 +0000
Subject: Fix bug #2473 due to wrong folding of the evar environment

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14573 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml4                         |  2 +-
 test-suite/bugs/closed/shouldsucceed/2473.v | 39 +++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2473.v

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 2af439550a..c2178229de 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -385,7 +385,7 @@ let unify_eqn env sigma hypinfo t =
     let res =
       if l2r then (prf, (car, rel, c1, c2))
       else
-	try (mkApp (get_symmetric_proof env Evd.empty car rel,
+	try (mkApp (get_symmetric_proof env env'.evd car rel,
 		   [| c1 ; c2 ; prf |]),
 	    (car, rel, c2, c1))
 	with Not_found ->
diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/shouldsucceed/2473.v
new file mode 100644
index 0000000000..4c3025128c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2473.v
@@ -0,0 +1,39 @@
+
+Require Import Relations Program Setoid Morphisms.
+
+Section S1.
+  Variable R: nat -> relation bool.
+  Instance HR1: forall n, Transitive (R n). Admitted.
+  Instance HR2: forall n, Symmetric (R n).  Admitted.
+  Hypothesis H: forall n a, R n (andb a a) a.
+  Goal forall n a b, R n b a.
+   intros. 
+   (* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *)
+   (* idem with setoid_rewrite *)
+(*    assert (HR2' := HR2 n). *)
+   rewrite <- H.                (* ok *)
+   admit.
+  Qed.
+End S1.
+
+Section S2.
+  Variable R: nat -> relation bool.
+  Instance HR: forall n, Equivalence (R n). Admitted.
+  Hypothesis H: forall n a, R n (andb a a) a.
+  Goal forall n a b, R n a b.
+   intros. rewrite <- H. admit.
+  Qed.
+End S2.
+
+(* the parametrised relation is required to get the problem *)
+Section S3.
+  Variable R: relation bool.
+  Instance HR1': Transitive R. Admitted.
+  Instance HR2': Symmetric R.  Admitted.
+  Hypothesis H: forall a, R (andb a a) a.
+  Goal forall a b, R b a.
+   intros. 
+   rewrite <- H.                (* ok *)
+   admit.
+  Qed.
+End S3.
\ No newline at end of file
-- 
cgit v1.2.3