diff options
| author | jouvelot | 2021-03-23 12:55:54 +0100 |
|---|---|---|
| committer | GitHub | 2021-03-23 12:55:54 +0100 |
| commit | 6d51f94b218cae4bd51ba268eff90b7c38c8f627 (patch) | |
| tree | 563560ce32bb68cb3b10d60b40fa0fbf67182962 | |
| parent | 8e859e628404c50c8191f30489abf4e799f46f8d (diff) | |
Update path.v
Typo in documentation.
| -rw-r--r-- | mathcomp/ssreflect/path.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index dd3e867..7087fc5 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 p. *) +(* 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 *) |
