Extras: remove duplicated definition

coq-community · Aug 14, 2020 · dc1d9f2 · dc1d9f2
1 parent 2fa52d2
commit dc1d9f2
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/.gitignore b/.gitignore
@@ -22,3 +22,4 @@ index.md
 *.coq.d
 *.vok
 *.vos
+.lia.cache
diff --git a/theories/Programming/Extras.v b/theories/Programming/Extras.v
@@ -23,10 +23,12 @@ Module FunNotation.
 End FunNotation.
 Import FunNotation.
 
-Definition compose A B C (g:B -> C) (f:A -> B) (x:A) : C := g (f x).
-
+(* Uncomment the following line after we drop Coq 8.8: *)
+(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
 Definition uncurry A B C (f:A -> B -> C) (x:A * B) : C := let (a,b) := x in f a b.
 
+(* Uncomment the following line after we drop Coq 8.8: *)
+(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
 Definition curry  {A B C} (f : A * B -> C) (a : A) (b : B) : C := f (a, b).
 
 Lemma uncurry_curry : forall A B C (f : A -> B -> C) a b,
@@ -44,8 +46,6 @@ Proof.
   reflexivity.
 Qed.
 
-Definition const A B (x:B) : A -> B := fun _ => x.
-
 Fixpoint zip A B (xs:list A) (ys:list B) : list (A * B) :=
   match xs, ys with
   | [], _ => []
-Original file line number
+Diff line change
@@ Expand Up / @@ -22,3 +22,4 @@ index.md @@
     *.coq.d
     *.vok
     *.vos
+    .lia.cache