diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/coercions.v | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 750165a55a..d652132e49 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -31,7 +31,7 @@ Parameter C:> forall n:nat, A n -> nat. *) (* Check coercion between products based on eta-expansion *) -(* (there was a de Bruijn bug until rev ) *) +(* (there was a de Bruijn bug until rev 9254) *) Section P. @@ -42,3 +42,22 @@ 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. + |