Remove ListUtil.List.repeat

We are no longer checking against Coq 8.5, and it's simpler to not have
two versions of `List.repeat` floating around.

1 files changed, 0 insertions, 23 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index fb19ac1da..60899696d 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -178,29 +178,6 @@ Module Export List.
     Qed.
   End Facts.
 
-  Section Repeat.
-
-    Variable A : Type.
-    Fixpoint repeat (x : A) (n: nat ) :=
-      match n with
-      | O => []
-      | S k => x::(repeat x k)
-      end.
-
-    Theorem repeat_length x n:
-      length (repeat x n) = n.
-    Proof using Type.
-      induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity.
-    Qed.
-
-    Theorem repeat_spec n x y:
-      In y (repeat x n) -> y=x.
-    Proof using Type.
-      induction n as [|k Hrec]; simpl; destruct 1; auto.
-    Qed.
-
-  End Repeat.
-
   Section Cutting.
 
     Variable A : Type.