aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Option.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2018-06-04 17:07:36 -0400
committerGravatar Jason Gross <jagro@google.com>2018-06-04 17:07:36 -0400
commitb4a0f83c3d9853cd2594bfb3f88adda5e783451e (patch)
tree530235c7d115d9e141506855601659dfb5fa9df9 /src/Util/Option.v
parent88d9d2c6e02c6a29e25fbfa90e92c5416a9c13d4 (diff)
Move Option.List.map to OptionList.map to fix name clashes in Tuple
Diffstat (limited to 'src/Util/Option.v')
-rw-r--r--src/Util/Option.v17
1 files changed, 0 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