Add Util.Option.bind2

To replace `RingMicromega.map_option2` in
#1609

src/Util/Notations.v

@@ -124,6 +124,11 @@ Reserved Notation "A <-- X ; B" (at level 70, X at next level, right associativi
 Reserved Notation "A <--- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <---  X ; '/' B ']'").
 Reserved Notation "A <---- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <----  X ; '/' B ']'").
 Reserved Notation "A <----- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <-----  X ; '/' B ']'").
+Reserved Notation "A , A' <- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <-  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <-- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <--  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <--- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <---  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <---- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <----  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <----- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <-----  X ,  X' ; '/' B ']'").
 Reserved Notation "A ;; B" (at level 70, right associativity, format "'[v' A ;; '/' B ']'").
 Reserved Notation "A ';;L' B" (at level 70, right associativity, format "'[v' A ';;L' '/' B ']'").
 Reserved Notation "A ';;R' B" (at level 70, right associativity, format "'[v' A ';;R' '/' B ']'").

src/Util/Option.v

@@ -35,6 +35,15 @@ Definition bind {A B} (v : option A) (f : A -> option B) : option B
      | None => None
      end.
 
+Definition bind2 {A B C} (v1 : option A) (v2 : option B) (f : A -> B -> option C) : option C
+  := match v1, v2 with
+     | None, _
+     | _, None
+       => None
+     | Some x1, Some x2 => f x1 x2
+     end.
+Global Arguments bind2 {A B C} !v1 !v2 / f.
+
 Definition sequence {A} (v1 v2 : option A) : option A
   := match v1 with
      | Some v => Some v
@@ -59,6 +68,7 @@ Module Export Notations.
 
   Notation "'olet' x .. y <- X ; B" := (bind X (fun x => .. (fun y => B%option) .. )) : option_scope.
   Notation "A <- X ; B" := (bind X (fun A => B%option)) : option_scope.
+  Notation "A , A' <- X , X' ; B" := (bind2 X X' (fun A A' => B%option)) : option_scope.
   Infix ";;" := sequence : option_scope.
   Infix ";;;" := sequence_return : option_scope.
 End Notations.