From 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 8 Sep 2008 00:15:04 +0200 Subject: Imported Upstream version 8.2~beta4.svn20080907+dfsg --- test-suite/success/coercions.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'test-suite/success/coercions.v') diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index d652132e..525348de 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