aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Basics.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Basics.v')
-rw-r--r--theories/Program/Basics.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 5293a66cb..7cef5c5ad 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -17,7 +17,7 @@
(** The polymorphic identity function is defined in [Datatypes]. *)
-Implicit Arguments id [[A]].
+Arguments id {A} x.
(** Function composition. *)
@@ -53,5 +53,5 @@ Definition apply {A B} (f : A -> B) (x : A) := f x.
(** Curryfication of [prod] is defined in [Logic.Datatypes]. *)
-Implicit Arguments prod_curry [[A] [B] [C]].
-Implicit Arguments prod_uncurry [[A] [B] [C]].
+Arguments prod_curry {A B C} f p.
+Arguments prod_uncurry {A B C} f x y.