diff options
Diffstat (limited to 'test-suite/success/coercions.v')
| -rw-r--r-- | test-suite/success/coercions.v | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 8dd48752..d652132e 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -22,7 +22,7 @@ Coercion i : h >-> nat. Parameter C : nat -> nat -> nat. Coercion C : nat >-> Funclass. -(* Remark: in the following example, it cannot be decide whether C is +(* Remark: in the following example, it cannot be decided whether C is from nat to Funclass or from A to nat. An explicit Coercion command is expected @@ -30,3 +30,34 @@ Parameter A : nat -> Prop. Parameter C:> forall n:nat, A n -> nat. *) +(* Check coercion between products based on eta-expansion *) +(* (there was a de Bruijn bug until rev 9254) *) + +Section P. + +Variable E : Set. +Variables C D : E -> Prop. +Variable G :> forall x, C x -> D x. + +Check fun (H : forall y:E, y = y -> C y) => (H : forall y:E, y = y -> D y). + +End P. + +(* Check that class arguments are computed the same when looking for a + coercion and when applying it (class_args_of) (failed until rev 9255) *) + +Section Q. + +Variable bool : Set. +Variables C D : bool -> Prop. +Variable G :> forall x, C x -> D x. +Variable f : nat -> bool. + +Definition For_all (P : nat -> Prop) := forall x, P x. + +Check fun (H : For_all (fun x => C (f x))) => H : forall x, D (f x). +Check fun (H : For_all (fun x => C (f x))) x => H x : D (f x). +Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)). + +End Q. + |