Move Option.List.map to OptionList.map to fix name clashes in Tuple

2 files changed, 20 insertions, 17 deletions

diff --git a/src/Util/Option.v b/src/Util/Option.v
index e14ad263e..b9e64910c 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -18,23 +18,6 @@ Module Export Notations.
 End Notations.
 Local Open Scope option_scope.
 
-Module List.
-  Section map.
-    Context {A B}
-            (f : A -> option B).
-
-    Fixpoint map (ls : list A) : list B
-      := match ls with
-         | nil => nil
-         | cons x xs
-           => match f x with
-              | Some fx => fx :: map xs
-              | None => map xs
-              end
-         end.
-  End map.
-End List.
-
 Section Relations.
   Definition option_eq {A} eq (x y : option A) :=
     match x with
diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v
new file mode 100644
index 000000000..57cc52f06
--- /dev/null
+++ b/src/Util/OptionList.v
@@ -0,0 +1,20 @@
+Require Import Crypto.Util.Notations.
+
+Module Option.
+  Module List.
+    Section map.
+      Context {A B}
+              (f : A -> option B).
+
+      Fixpoint map (ls : list A) : list B
+        := match ls with
+           | nil => nil
+           | cons x xs
+             => match f x with
+               | Some fx => fx :: map xs
+               | None => map xs
+               end
+           end.
+    End map.
+  End List.
+End Option.