diff options
| author | Kazuhiko Sakaguchi | 2020-11-18 13:33:36 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-19 05:53:45 +0900 |
| commit | 9e6c20b4bd5397539debee9fcb0853b6924ecfb9 (patch) | |
| tree | 512c6cc466df5609008bb339a1a2a67dd59df44d | |
| parent | 82db85f541dc9a47fd79b462a63b8b80a8468557 (diff) | |
Rename `subseq_order_path` to `subseq_path`
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 6 |
2 files changed, 6 insertions, 1 deletions
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). |