From c34596ab97743ddc3761f72f61edfd856bd2804e Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Mon, 20 Jul 2020 21:59:37 -0400
Subject: deprecate prod_curry and prod_uncurry

---
 theories/Init/Datatypes.v | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 8ab12ae534..77be679070 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -272,12 +272,18 @@ Proof with auto.
   - destruct H; subst...
 Qed.
 
-Definition prod_uncurry (A B C:Type) (f:A * B -> C)
+Definition curry {A B C:Type} (f:A * B -> C)
   (x:A) (y:B) : C := f (x,y).
 
-Definition prod_curry (A B C:Type) (f:A -> B -> C)
+Definition uncurry {A B C:Type} (f:A -> B -> C)
   (p:A * B) : C := match p with (x, y) => f x y end.
 
+#[deprecated(since = "8.13", note = "Use curry instead.")]
+Definition prod_uncurry (A B C:Type) : (A * B -> C) -> A -> B -> C := curry.
+
+#[deprecated(since = "8.13", note = "Use uncurry instead.")]
+Definition prod_curry (A B C:Type) : (A -> B -> C) -> A * B -> C := uncurry.
+
 Import EqNotations.
 
 Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2),
-- 
cgit v1.2.3