Fix bugs introduced by previous commit

3 files changed, 3 insertions, 3 deletions

diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v
index 9c796ad57..a597b7bf2 100644
--- a/src/Arithmetic/Saturated/Core.v
+++ b/src/Arithmetic/Saturated/Core.v
@@ -398,7 +398,7 @@ Module Columns.
     Lemma map_sum_nils n : map sum (nils n) = B.Positional.zeros n.
     Proof using Type.
       cbv [nils B.Positional.zeros]; induction n as [|n]; [reflexivity|].
-      change (repeat nil (S n)) with (@nil Z :: repeat nil n).
+      change (List.repeat nil (S n)) with (@nil Z :: List.repeat nil n).
       rewrite Tuple.map_repeat, sum_nil. reflexivity.
     Qed.
 
diff --git a/src/Compilers/FilterLive.v b/src/Compilers/FilterLive.v
index 5f3f0156d..f54a8febb 100644
--- a/src/Compilers/FilterLive.v
+++ b/src/Compilers/FilterLive.v
@@ -46,7 +46,7 @@ Section language.
             match ns with
             | Some n =>
               @filter_live_namesf
-                (prefix ++ repeat dead_name (count_pairs tx))%list remaining' _
+                (prefix ++ List.repeat dead_name (count_pairs tx))%list remaining' _
                 (eC (SmartValf (fun _ => list Name) (fun _ => namesx ++ names_to_list n)%list _))
             | None => nil
             end
diff --git a/src/LegacyArithmetic/Double/Core.v b/src/LegacyArithmetic/Double/Core.v
index b7be2d18a..53f20801c 100644
--- a/src/LegacyArithmetic/Double/Core.v
+++ b/src/LegacyArithmetic/Double/Core.v
@@ -20,7 +20,7 @@ Local Notation eta x := (fst x, snd x).
 
 (** The list is low to high; the tuple is low to high *)
 Definition tuple_decoder {n W} {decode : decoder n W} {k : nat} : decoder (k * n) (tuple W k)
-  := {| decode w := BaseSystem.decode (Pow2Base.base_from_limb_widths (repeat n k))
+  := {| decode w := BaseSystem.decode (Pow2Base.base_from_limb_widths (List.repeat n k))
                                       (List.map decode (List.rev (Tuple.to_list _ w))) |}.
 Global Arguments tuple_decoder : simpl never.
 Hint Extern 3 (decoder _ (tuple ?W ?k)) => let kv := (eval simpl in (Z.of_nat k)) in apply (fun n decode => (@tuple_decoder n W decode k : decoder (kv * n) (tuple W k))) : typeclass_instances.