From 307c7610df6389768848e574170da85f1ab2c8fe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 Sep 2008 10:06:21 +0000
Subject: Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about
 backtracking on coercion classes when a coercion path fails).

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

(limited to 'test-suite')

diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index d652132e49..525348dec9 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -61,3 +61,24 @@ Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)).
 
 End Q.
 
+(* Combining class lookup and path lookup so that if a lookup fails, another
+   descent in the class can be found (see wish #1934) *)
+
+Record Setoid : Type :=
+{ car :>  Type }.
+
+Record Morphism (X Y:Setoid) : Type :=
+{evalMorphism :> X -> Y}.
+
+Definition extSetoid (X Y:Setoid) : Setoid.
+intros X Y.
+constructor.
+exact (Morphism X Y).
+Defined.
+
+Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x.
+
+Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
+
+Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
+
-- 
cgit v1.2.3