diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-02 10:06:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-02 10:06:21 +0000 |
| commit | 307c7610df6389768848e574170da85f1ab2c8fe (patch) | |
| tree | 656e753eb1fd5c1863385b0d27b552ed7643ca10 /test-suite/success | |
| parent | 653f63e8b49fd46e686619d8e847e571d8c5442a (diff) | |
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
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/coercions.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index d652132e4..525348dec 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. + |