diff options
| author | Enrico Tassi | 2020-04-02 12:14:12 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-02 12:14:12 +0200 |
| commit | 0ce6013351c60f0abd4445c9eeccdd3749b071ec (patch) | |
| tree | 85194f55821511391f2aca58f346cbfd82012aed /mathcomp/ssreflect/seq.v | |
| parent | e44b131a6c01c9cac13b48b07e3ee4d7f8e8fb6c (diff) | |
| parent | a8c8fd1f52f90606f5aaf4f4b810b70aabc9caa2 (diff) | |
Merge pull request #468 from ybertot/remove-deprecated-from-1.9
remove deprecated commands whose deprecation was introduced in 1.9.0
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index ed7c1dd..6dc739e 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -3426,21 +3426,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 _ _ _) |