aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/ssreflect/seq.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index c658ac2..3d56831 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -126,7 +126,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
(* s and t, respectively, in row-major order, *)
(* and where t is possibly dependent in elements of s *)
(* allpairs_dep f s t := self expanding definition for *)
-(* [seq f x y | x <- s, y <- t i] *)
+(* [seq f x y | x <- s, y <- t y] *)
(* ** Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m], *)
(* allpairs f s t := same as allpairs_dep but where t is non dependent, *)
(* i.e. self expanding definition for *)