aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
diff options
context:
space:
mode:
authorjouvelot2021-03-23 14:16:30 +0100
committerGitHub2021-03-23 14:16:30 +0100
commit7fa73806c771ad682d0bdca6de01f8d51e1462d1 (patch)
treef3b0ff89046f228e2ce4ed34adf1c41e300af173 /mathcomp/ssreflect
parent6d51f94b218cae4bd51ba268eff90b7c38c8f627 (diff)
Update mathcomp/ssreflect/path.v
Sure. Thanks. Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
Diffstat (limited to 'mathcomp/ssreflect')
-rw-r--r--mathcomp/ssreflect/path.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 7087fc5..a252f50 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -73,7 +73,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
(* of splitP will also simultaneously replace take (index x p) with p1 and *)
(* drop (index x p).+1 p with p2. *)
(* - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and *)
-(* simultaneously generates an equation x = last x0 p1. *)
+(* simultaneously generates an equation x = last x0 p1. *)
(* - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x *)
(* appears explicitly at the start of the right part. *)
(* The parts p1 and p2 are computed using index/take/drop in all cases, but *)