diff options
author | Jason Gross <jagro@google.com> | 2018-06-04 17:07:36 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-06-04 17:07:36 -0400 |
commit | b4a0f83c3d9853cd2594bfb3f88adda5e783451e (patch) | |
tree | 530235c7d115d9e141506855601659dfb5fa9df9 /src/Util/Option.v | |
parent | 88d9d2c6e02c6a29e25fbfa90e92c5416a9c13d4 (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.v | 17 |
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 |