From 7fa73806c771ad682d0bdca6de01f8d51e1462d1 Mon Sep 17 00:00:00 2001 From: jouvelot Date: Tue, 23 Mar 2021 14:16:30 +0100 Subject: Update mathcomp/ssreflect/path.v Sure. Thanks. Co-authored-by: Kazuhiko Sakaguchi --- mathcomp/ssreflect/path.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/ssreflect') 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 *) -- cgit v1.2.3