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

2 files changed, 40 insertions, 1 deletions

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