diff options
Diffstat (limited to 'test-suite/output/Coercions.v8')
| -rw-r--r-- | test-suite/output/Coercions.v8 | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/test-suite/output/Coercions.v8 b/test-suite/output/Coercions.v8 deleted file mode 100644 index f3a09f3c2..000000000 --- a/test-suite/output/Coercions.v8 +++ /dev/null @@ -1,15 +0,0 @@ -(* Submitted by Randy Pollack *) - -Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. - -Section testSection. -Variables (S : Set) (P : pred S) (R : rel S) (x : S). -Check (P x). -Check (R x x). -End testSection. - -(* Check the removal of coercions with target Funclass *) - -Record foo : Type := {D :> nat -> nat}. -Check (fun (x : foo) (n : nat) => x n).
\ No newline at end of file |