Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

remove deprecated commands whose deprecation was introduced in 1.9.0 #468

Merged
merged 1 commit into from Apr 2, 2020
Merged

remove deprecated commands whose deprecation was introduced in 1.9.0 #468

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
14 changes: 14 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Expand Up @@ -125,6 +125,20 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).

### Removed

The following were deprecated since release 1.9.0
- `tuple_perm_eqP` (use `tuple_permP` instead, from `perm.v`)
- `eq_big_perm` (use `perm_big` instead, from `bigop.v`)
- `perm_eqP` (use `permP` instead, from seq.v)
- `perm_eqlP` (use `permPl` instead)
- `perm_eqrP` (use `permPr` instead)
- `perm_eqlE` (use `permEl` instead)
- `perm_eq_refl` (use `perm_refl` instead)
- `perm_eq_sym` (use `perm_sym` instead)
- `perm_eq_trans` (use `perm_trans` instead)
- `perm_eq_size` (use `perm_size` instead)
- `perm_eq_mem` (use `perm_mem` instead)
- `perm_eq_uniq` (use `perm_uniq` instead)

### Infrastructure

### Misc
4 changes: 0 additions & 4 deletions mathcomp/fingroup/perm.v
View file
Open in desktop
Expand Up @@ -576,7 +576,3 @@ Qed.
End LiftPerm.

Prenex Implicits lift_perm lift_permK.

Notation tuple_perm_eqP :=
(deprecate tuple_perm_eqP tuple_permP) (only parsing).

7 changes: 0 additions & 7 deletions mathcomp/ssreflect/bigop.v
View file
Open in desktop
Expand Up @@ -1937,13 +1937,6 @@ Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed.
Arguments biggcdn_inf [I] i0 [P F m].

Notation "@ 'eq_big_perm'" :=
(deprecate eq_big_perm perm_big) (at level 10, only parsing).

Notation eq_big_perm :=
((fun R idx op I r1 P F r2 => @eq_big_perm R idx op I r1 r2 P F)
_ _ _ _ _ _ _) (only parsing).

Notation filter_index_enum :=
((fun _ => @deprecated_filter_index_enum _)
(deprecate filter_index_enum big_enumP)) (only parsing).
15 changes: 0 additions & 15 deletions mathcomp/ssreflect/seq.v
View file
Open in desktop
Expand Up @@ -3430,21 +3430,6 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
Ltac tfae := do !apply: AllIffConj.

(* Temporary backward compatibility. *)
Notation perm_eqP := (deprecate perm_eqP permP) (only parsing).
Notation perm_eqlP := (deprecate perm_eqlP permPl) (only parsing).
Notation perm_eqrP := (deprecate perm_eqrP permPr) (only parsing).
Notation perm_eqlE := (deprecate perm_eqlE permEl _ _ _) (only parsing).
Notation perm_eq_refl := (deprecate perm_eq_refl perm_refl _) (only parsing).
Notation perm_eq_sym := (deprecate perm_eq_sym perm_sym _) (only parsing).
Notation "@ 'perm_eq_trans'" := (deprecate perm_eq_trans perm_trans)
(at level 10, only parsing).
Notation perm_eq_trans := (@perm_eq_trans _ _ _ _) (only parsing).
Notation perm_eq_size := (deprecate perm_eq_size perm_size _ _ _)
(only parsing).
Notation perm_eq_mem := (deprecate perm_eq_mem perm_mem _ _ _)
(only parsing).
Notation perm_eq_uniq := (deprecate perm_eq_uniq perm_uniq _ _ _)
(only parsing).
Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _)
(only parsing).
Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _)
Expand Down