From 6d51f94b218cae4bd51ba268eff90b7c38c8f627 Mon Sep 17 00:00:00 2001
From: jouvelot
Date: Tue, 23 Mar 2021 12:55:54 +0100
Subject: Update path.v

Typo in documentation.---
 mathcomp/ssreflect/path.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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   *)
-- 
cgit v1.2.3