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

1 files changed, 39 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/shouldsucceed/2473.v
new file mode 100644
index 000000000..4c3025128
--- /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