From 9e6c20b4bd5397539debee9fcb0853b6924ecfb9 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 18 Nov 2020 13:33:36 +0900
Subject: Rename `subseq_order_path` to `subseq_path`

---
 CHANGELOG_UNRELEASED.md   | 1 +
 mathcomp/ssreflect/path.v | 6 +++++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 58eb93d..f2ba40b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -425,6 +425,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + `eq_sorted(_irr)` -> `(irr_)sorted_eq`
   + `sorted_(lt|le)_nth` -> `sorted_(ltn|leq)_nth`
   + `(ltn|leq)_index` -> `sorted_(ltn|leq)_index`
+  + `subseq_order_path` -> `subseq_path`
 
 - in `div.v`
   + `coprime_mul(l|r)` -> `coprimeM(l|r)`
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 5638371..72c9719 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -419,7 +419,7 @@ Local Notation sorted := (sorted leT).
 
 Hypothesis leT_tr : transitive leT.
 
-Lemma subseq_order_path x s1 s2 : subseq s1 s2 -> path x s2 -> path x s1.
+Lemma subseq_path x s1 s2 : subseq s1 s2 -> path x s2 -> path x s1.
 Proof. by case/subseqP => m _ ->; apply/path_mask. Qed.
 
 Lemma subseq_sorted s1 s2 : subseq s1 s2 -> sorted s2 -> sorted s1.
@@ -1454,6 +1454,8 @@ Notation "@ 'ltn_index'" := (deprecate ltn_index sorted_ltn_index)
   (at level 10, only parsing) : fun_scope.
 Notation "@ 'leq_index'" := (deprecate leq_index sorted_leq_index)
   (at level 10, only parsing) : fun_scope.
+Notation "@ 'subseq_order_path'" := (deprecate subseq_order_path subseq_path)
+  (at level 10, only parsing) : fun_scope.
 
 Notation eq_sorted :=
   (fun le_tr le_asym => @eq_sorted _ _ le_tr le_asym _ _) (only parsing).
@@ -1470,3 +1472,5 @@ Notation ltn_index :=
 Notation leq_index :=
   (fun leT_tr leT_refl s_sorted =>
      @leq_index _ _ leT_tr leT_refl _ s_sorted _ _) (only parsing).
+Notation subseq_order_path :=
+  (fun leT_tr => @subseq_order_path _ _ leT_tr _ _ _) (only parsing).
-- 
cgit v1.2.3