Uniformisation of some error messages + added test on setoid rewrite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11765 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index f49f58e5a..be5999df5 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -116,3 +116,17 @@ Add Morphism (@f A) : f_morph.
 Proof.
 unfold rel, f. trivial.
 Qed.
+
+(* Submitted by Nicolas Tabareau *)
+(* Needs unification.ml to support environments with de Bruijn *)
+
+Goal forall
+  (f : Prop -> Prop)
+  (Q : (nat -> Prop) -> Prop)
+  (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True)
+  (h:nat -> Prop), 
+  Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True.
+intros f0 Q H.
+setoid_rewrite H.
+tauto.
+Qed.