diff options
| author | Yves Bertot | 2020-03-31 17:33:14 +0200 |
|---|---|---|
| committer | Yves Bertot | 2020-03-31 17:55:10 +0200 |
| commit | a8c8fd1f52f90606f5aaf4f4b810b70aabc9caa2 (patch) | |
| tree | b0e84f62af50e8b8df4de7399bf87af12ddaded8 /mathcomp/ssreflect | |
| parent | 06048e6125b430133e3eb2102e166545f5f804f2 (diff) | |
remove deprecated commands whose deprecation was introduced in release 1.9.0
fixes #418
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 7 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 15 |
2 files changed, 0 insertions, 22 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 6d18825..633bb36 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -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). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index f73c119..86a1545 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -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 _ _ _) |