diff options
Diffstat (limited to 'theories/Program/Basics.v')
| -rw-r--r-- | theories/Program/Basics.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 4bc29a071..e5be0ca92 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -15,8 +15,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* Set Universe Polymorphism. *) - (** The polymorphic identity function is defined in [Datatypes]. *) Arguments id {A} x. @@ -47,7 +45,7 @@ Definition const {A B} (a : A) := fun _ : B => a. (** The [flip] combinator reverses the first two arguments of a function. *) -Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x. +Definition flip {A B C} (f : A -> B -> C) x y := f y x. (** Application as a combinator. *) |