Skip to content

Latest commit

 

History

History
177 lines (138 loc) · 6.49 KB

CHANGELOG_UNRELEASED.md

File metadata and controls

177 lines (138 loc) · 6.49 KB

Changelog (unreleased)

To avoid having old PRs put changes into the wrong section of the CHANGELOG, new entries now go to the present file as discussed here.

The format is based on Keep a Changelog.

[Unreleased]

Added

  • in seq.v

    • lemmas subset_mapP, take_min, take_taker, perm_allpairs_dep, perm_allpairs
  • in path.v

    • lemmas prefix_path, prefix_sorted, infix_sorted, suffix_sorted
  • in ssralg.v

    • lemmas natr1, nat1r, telescope_sumr_eq, telescope_prodr_eq, telescope_prodf_eq
  • in poly.v

    • definitions even_poly, odd_poly, take_poly, drop_poly
    • lemmas comm_polyD, comm_polyM, comm_poly_exp, root_exp, root_ZXsubC, size_mulXn, coef_sumMXn, comp_Xn_poly, coef_comp_poly_Xn, comp_poly_Xn, size_even_poly, size_even_poly_eq, coef_even_poly, even_polyE, even_polyD, even_polyZ, even_poly_is_linear, even_polyC, size_odd_poly, coef_odd_poly, odd_polyE, odd_polyC, odd_polyD, odd_polyZ, odd_poly_is_linear, odd_polyMX, even_polyMX, sum_even_poly, sum_odd_poly, poly_even_odd, size_take_poly, coef_take_poly, take_poly_id, take_polyD, take_polyZ, take_poly_is_linear, take_poly_sum, take_poly0l, take_poly0r, take_polyMXn, take_polyMXn_0, take_polyDMXn, size_drop_poly, size_drop_poly_eq, coef_drop_poly, drop_poly_eq0, sum_drop_poly, drop_polyD, drop_polyZ, drop_poly_is_linear, drop_poly_sum, drop_poly0l, drop_poly0r, drop_polyMXn, drop_polyMXn_id, drop_polyDMXn, poly_take_drop, eqp_take_drop, scale_polyC
    • canonical instances even_poly_additive, even_poly_linear, odd_poly_additive, odd_poly_linear, take_poly_additive, take_poly_linear, drop_poly_additive, drop_poly_linear
  • in polydiv.v

    • lemmas Pdiv.RingMonic.drop_poly_rdivp, Pdiv.RingMonic.take_poly_rmodp, Pdiv.IdomainMonic.drop_poly_divp, Pdiv.IdomainMonic.take_poly_modp
  • in bigop.v

    • lemmas big_ord1_eq, big_ord1_cond_eq, big_nat1_eq, big_nat1_cond_eq
  • in eqtype.v

    • lemmas existsb and exists_inb
  • in seq.v

    • lemma if_nth
  • in ssrbool.v

    • lemmas if_and, if_or, if_implyb, if_impliybC, if_add
  • in ssralg.v

    • lemma eqr_sum_div
  • in ssrnum.v

    • lemmas psumr_neq0, psumr_neq0P
  • in ssrnat.v

    • lemma leqVgt
    • lemmas ltn_half_double, leq_half_double, gtn_half_double
    • lemma double_pred
    • lemmas uphalfE, ltn_uphalf_double, geq_uphalf_double, gtn_uphalf_double
    • lemmas halfK, uphalfK, odd_halfK, even_halfK, odd_uphalfK, even_uphalfK
    • lemmas leq_sub2rE, leq_sub2lE, ltn_sub2rE, ltn_sub2lE
  • in ssrint.v

    • printing only notation for x = y :> int, opening int_scope on x and y to better match the already existing parsing only notation with the introduction of number notations in ring_scope
  • in bigop.v

    • lemmas big_seq1_id, big_nat1_id, big_pred1_eq_id, big_pred1_id, big_const_idem, big1_idem, big_id_idem, big_rem_AC, perm_big_AC, big_enum_cond_AC, bigD1_AC, bigD1_seq_AC, big_image_cond_AC, big_image_AC, big_image_cond_id_AC, Lemma, cardD1x, reindex_omap_AC, reindex_onto_AC, reindex_AC, reindex_inj_AC, bigD1_ord_AC, big_enum_val_cond_AC, big_enum_rank_cond_AC, big_nat_rev_AC, big_rev_mkord_AC, big_mkcond_idem, big_mkcondr_idem, big_mkcondl_idem, big_rmcond_idem, big_rmcond_in_idem, big_cat_idem, big_allpairs_dep_idem, big_allpairs_idem, big_cat_nat_idem, big_split_idem, big_id_idem_AC, bigID_idem, bigU_idem, partition_big_idem, sig_big_dep_idem, pair_big_dep_idem, pair_big_idem, pair_bigA_idem, exchange_big_dep_idem, exchange_big_idem, exchange_big_dep_nat_idem, exchange_big_nat_idem, big_undup_AC
  • in matrix.v

    • definitions Vandrmonde, map2_mx
    • lemma det_Vandermonde, map2_trmx, map2_const_mx, map2_row, map2_col, map2_row', map2_col', map2_mxsub, map2_row_perm, map2_col_perm, map2_xrow, map2_xcol, map2_castmx, map2_conform_mx, map2_mxvec, map2_vec_mx, map2_row_mx, map2_col_mx, map2_block_mx, map2_lsubmx, map2_rsubmx, map2_usubmx, map2_dsubmx, map2_ulsubmx, map2_ursubmx, map2_dlsubmx, map2_drsubmx, eq_in_map2_mx, eq_map2_mx, map2_mx_left_in, map2_mx_left, map2_mx_right_in, map2_mx_right, map2_mxA, map2_1mx, map2_mx1, map2_mxC, map2_0mx, map2_mx0, map2_mxDl, map2_mxDr, diag_mx_is_additive, mxtrace_is_additive
  • in ssralg.v

    • lemmas divrN, divrNN

Changed

  • in poly.v:

    • generalize eq_poly
  • in poly.v:

    • made hornerE preserve powers
  • in matrix.v:

    • updated oppmx, addmx, addmxA, addmxC, add0mx
    • moved to an earlier section of the file diag_mx, tr_diag_mx, diag_mx_row, diag_mxP, diag_mx_is_diag, diag_mx_is_trig, scalar_mx, diag_const_mx, tr_scalar_mx, scalar_mx_is_additive, is_scalar_mx, is_scalar_mxP, scalar_mx_is_scalar, mx0_is_scalar, scalar_mx_is_diag, is_scalar_mx_is_diag, scalar_mx_is_trig, is_scalar_mx_is_trig, mx11_scalar, scalar_mx_block, mxtrace, mxtrace_tr, mxtrace0, mxtraceD, mxtrace_diag, mxtrace_scalar, trace_mx11, mxtrace_block

Renamed

Removed

  • in matrix.v:

    • notation card_matrix (deprecated in 1.13.0)
  • in rat.v:

    • notation divq_eq (deprecated in 1.13.0)
  • in ssralg.v:

    • notation prodr_natmul (deprecated in 1.13.0)
  • in bigop.v:

    • notation big_uncond (deprecated in 1.13.0)
  • in finset.v:

    • notations mem_imset_eq and mem_imset2_eq (deprecated in 1.13.0)
  • in order.v:

    • notations join_sup_seq, join_min_seq, join_sup, join_min, join_seq, meet_inf_seq, meet_max_seq, meet_seq (deprecated in 1.13.0)
  • in path.v:

    • notations sup_path_in, sub_cycle_in, sub_sorted_in, eq_path_in, eq_cycle_in (deprecated in 1.13.0)
  • in seq.v:

    • notation iota_add (deprecated in 1.13.0)
  • in ssreflect.v:

    • module Deprecation (deprecated in 1.13.0)
    • notatin deprecate (deprecated in 1.13.0)
  • in ssrnat.v:

    • notatin fact_smonotone (deprecated in 1.13.0)

Infrastructure

Misc