From a96b65816bdbbd7b253ccc0920803d7a1da0ae75 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 15 Mar 2007 16:58:50 +0000
Subject: Test de non-régression pour commit 9673

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9709 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/setoid_test.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index dd1022f089..e99b3c19bb 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -104,3 +104,15 @@ setoid_rewrite <- H.
 trivial.
 Qed.
 
+(* Unifying the domain up to delta-conversion (example from emakarov) *)
+
+Definition id: Set -> Set := fun A => A.
+Definition rel : forall A : Set, relation (id A) := @eq.
+Definition f: forall A : Set, A -> A := fun A x => x.
+
+Add Relation id rel as eq_rel.
+
+Add Morphism f with signature rel ++> rel as f_morph.
+Proof.
+unfold rel, f. trivial.
+Qed.
-- 
cgit v1.2.3