Add notations for patterns in [seq ... ] notations

This allows syntax such as
```coq
Check [seq '(x, y) <- List.combine (List.seq 0 5) (List.seq 0 5) | x == y ].
Check [seq x + y | '(x, y) <- List.combine (List.seq 5 5) (List.seq 5 5) ].
```
to parse and print.

CHANGELOG_UNRELEASED.md

@@ -30,6 +30,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + new lemmas `cat_nilp`, `rev_nilp`, `allrelT`, `allrel_relI`, and
     `pairwise_relI`.
   + new lemma `undup_map_inj`.
+  + notations `[seq x <- s | C ]`, `[seq x <- s | C1 & C2 ]`, `[seq E
+    | i <- s ]`, `[seq E | i <- s & C ]`, `[seq E : R | i <- s ]`,
+    `[seq E : R | i <- s & C ]`, `[seq E | x <- s, y <- t ]`, `[seq
+    E : R | x <- s, y <- t ]` now support destructuring patterns in
+    binder positions.
 
 - in `path.v`, new lemmas: `sorted_pairwise(_in)`, `path_pairwise(_in)`,
   `cycle_all2rel(_in)`, `pairwise_sort`, and `sort_pairwise_stable`.

mathcomp/ssreflect/seq.v

@@ -940,6 +940,12 @@ Notation "[ 'seq' x <- s | C ]" := (filter (fun x => C%B) s)
 Notation "[ 'seq' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
  (at level 0, x at level 99,
   format "[ '[hv' 'seq'  x  <-  s '/ '  |  C1 '/ '  &  C2 ] ']'") : seq_scope.
+Notation "[ 'seq' ' x <- s | C ]" := (filter (fun x => C%B) s)
+ (at level 0, x strict pattern,
+  format "[ '[hv' 'seq'  ' x  <-  s '/ '  |  C ] ']'") : seq_scope.
+Notation "[ 'seq' ' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
+ (at level 0, x strict pattern,
+  format "[ '[hv' 'seq'  ' x  <-  s '/ '  |  C1 '/ '  &  C2 ] ']'") : seq_scope.
 Notation "[ 'seq' x : T <- s | C ]" := (filter (fun x : T => C%B) s)
  (at level 0, x at level 99, only parsing).
 Notation "[ 'seq' x : T <- s | C1 & C2 ]" := [seq x : T <- s | C1 && C2]
@@ -2399,32 +2405,18 @@ Proof. by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->]. Qed.
 End Map.
 
 Notation "[ 'seq' E | i <- s ]" := (map (fun i => E) s)
-  (at level 0, E at level 99, i ident,
+  (at level 0, E at level 99, i binder,
    format "[ '[hv' 'seq'  E '/ '  |  i  <-  s ] ']'") : seq_scope.
 
 Notation "[ 'seq' E | i <- s & C ]" := [seq E | i <- [seq i <- s | C]]
-  (at level 0, E at level 99, i ident,
+  (at level 0, E at level 99, i binder,
    format "[ '[hv' 'seq'  E '/ '  |  i  <-  s '/ '  &  C ] ']'") : seq_scope.
 
-Notation "[ 'seq' E | i : T <- s ]" := (map (fun i : T => E) s)
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
-
-Notation "[ 'seq' E | i : T <- s & C ]" :=
-  [seq E | i : T <- [seq i : T <- s | C]]
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
-
 Notation "[ 'seq' E : R | i <- s ]" := (@map _ R (fun i => E) s)
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+  (at level 0, E at level 99, i binder, only parsing) : seq_scope.
 
 Notation "[ 'seq' E : R | i <- s & C ]" := [seq E : R | i <- [seq i <- s | C]]
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
-
-Notation "[ 'seq' E : R | i : T <- s ]" := (@map T R (fun i : T => E) s)
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
-
-Notation "[ 'seq' E : R | i : T <- s & C ]" :=
-  [seq E : R | i : T <- [seq i : T <- s | C]]
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+  (at level 0, E at level 99, i binder, only parsing) : seq_scope.
 
 Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
 Proof. by elim: s => //= x s <-; case: (a x). Qed.
@@ -3307,18 +3299,12 @@ Arguments flatten_mapP {S T A s y}.
 
 Notation "[ 'seq' E | x <- s , y <- t ]" :=
   (flatten [seq [seq E | y <- t] | x <- s])
-  (at level 0, E at level 99, x ident, y ident,
+  (at level 0, E at level 99, x binder, y binder,
    format "[ '[hv' 'seq'  E '/ '  |  x  <-  s , '/   '  y  <-  t ] ']'")
    : seq_scope.
-Notation "[ 'seq' E | x : S <- s , y : T <- t ]" :=
-  (flatten [seq [seq E | y : T <- t] | x : S  <- s])
-  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
-Notation "[ 'seq' E : R | x : S <- s , y : T <- t ]" :=
-  (flatten [seq [seq E : R | y : T <- t] | x : S  <- s])
-  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
 Notation "[ 'seq' E : R | x <- s , y <- t ]" :=
   (flatten [seq [seq E : R | y <- t] | x  <- s])
-  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
+  (at level 0, E at level 99, x binder, y binder, only parsing) : seq_scope.
 
 Section AllPairsDep.