From e4542668e6d348e0300e76bb77105af24aff4233 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 19 Apr 2021 19:08:08 +0200
Subject: Use List.repeat from Coq's standard library instead of list_repeat

---
 lib/Coqlib.v | 20 --------------------
 1 file changed, 20 deletions(-)

(limited to 'lib')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index bd52d20a..e0789078 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -1153,26 +1153,6 @@ Proof.
   destruct l; simpl; auto.
 Qed.
 
-(** A list of [n] elements, all equal to [x]. *)
-
-Fixpoint list_repeat {A: Type} (n: nat) (x: A) {struct n} :=
-  match n with
-  | O => nil
-  | S m => x :: list_repeat m x
-  end.
-
-Lemma length_list_repeat:
-  forall (A: Type) n (x: A), length (list_repeat n x) = n.
-Proof.
-  induction n; simpl; intros. auto. decEq; auto.
-Qed.
-
-Lemma in_list_repeat:
-  forall (A: Type) n (x: A) y, In y (list_repeat n x) -> y = x.
-Proof.
-  induction n; simpl; intros. elim H. destruct H; auto.
-Qed.
-
 (** * Definitions and theorems over boolean types *)
 
 Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool :=
-- 
cgit