Rename ListUtil.map2 => ListUtil.List.map2

src/Util/ListUtil.v

@@ -337,6 +337,19 @@ Module Export List.
   (** new operations *)
   Definition enumerate {A} (ls : list A) : list (nat * A)
     := combine (seq 0 (length ls)) ls.
+
+  Section map2.
+    Context {A B C}
+      (f : A -> B -> C).
+
+    Fixpoint map2 (la : list A) (lb : list B) : list C :=
+      match la, lb with
+      | nil, _ => nil
+      | _, nil => nil
+      | a :: la', b :: lb'
+        => f a b :: map2 la' lb'
+      end.
+  End map2.
 End List.
 
 #[global]
@@ -371,19 +384,6 @@ Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l).
 
 Definition sum xs := sum_firstn xs (length xs).
 
-Section map2.
-  Context {A B C}
-          (f : A -> B -> C).
-
-  Fixpoint map2 (la : list A) (lb : list B) : list C :=
-    match la, lb with
-    | nil, _ => nil
-    | _, nil => nil
-    | a :: la', b :: lb'
-      => f a b :: map2 la' lb'
-    end.
-End map2.
-
 (* xs[n] := f xs[n] *)
 Fixpoint update_nth {T} n f (xs:list T) {struct n} :=
         match n with
@@ -3481,7 +3481,7 @@ Module Reifiable.
       intros H. induction l as [| x' l'].
       - simpl in H. destruct H.
       - simpl in H. destruct H as [H|H].
-        + rewrite H. clear H. simpl. destruct (existsb (eqb x) (nodupb l')) eqn:E. 
+        + rewrite H. clear H. simpl. destruct (existsb (eqb x) (nodupb l')) eqn:E.
           -- rewrite existsb_eqb_true_iff in E. rewrite <- nodupb_in_iff in E.
              apply IHl' in E. apply E.
           -- exists []. exists (nodupb l'). split.

src/Util/Tuple.v

@@ -315,7 +315,7 @@ Proof using Type.
 Qed.
 
 Lemma to_list_map2 {A B C n xs ys} (f : A -> B -> C)
-  : ListUtil.map2 f (@to_list A n xs) (@to_list B n ys) = @to_list C n (map2 f xs ys).
+  : List.map2 f (@to_list A n xs) (@to_list B n ys) = @to_list C n (map2 f xs ys).
 Proof using Type.
   tuples_from_lists; unfold map2, on_tuple2.
   repeat (rewrite to_list_from_list || rewrite from_list_to_list).
@@ -388,7 +388,7 @@ Proof using Type.
   destruct lxs as [|x' lxs']; [simpl in *; discriminate|].
   let lys := match goal with lxs : list B |- _ => lxs end in
   destruct lys as [|y' lys']; [simpl in *; discriminate|].
-  change ( f x y ::  ListUtil.map2 f (to_list (S n) (from_list (S n) (x' :: lxs') x1))
+  change ( f x y ::  List.map2 f (to_list (S n) (from_list (S n) (x' :: lxs') x1))
     (to_list (S n) (from_list (S n) (y' :: lys') x0)) = f x y :: to_list (S n) (map2 f (from_list (S n) (x' :: lxs') x1) (from_list (S n) (y' :: lys') x0)) ).
   tuple_maps_to_list_maps.
   reflexivity.