changelog for classical

CHANGELOG_UNRELEASED.md

@@ -12,6 +12,62 @@
 
 ### Changed
 
+- in `boolp.v`:
+  + in lemma `gen_choiceMixin`: `Choice.mixin_of` -> `hasChoice`
+  + in definition `gen_eqMixin`: `EqMixin` -> `hasDecEq.Build`
+  + canonical `dep_arrow_eqType` -> instance using `gen_eqMixin`
+  + canonical `dep_arrow_choiceType` -> instance using `gen_choiceMixin`
+  + canonical `Prop_eqType` -> instance using `gen_eqMixin`
+  + canonical `Prop_choiceType` -> instance using `gen_choiceMixin`
+  + canonical `classicType_eqType` -> instance using `gen_eqMixin`
+  + canonical `classicType_choiceType` -> instance using `gen_choiceMixin`
+  + canonical `eclassicType_eqType` -> instance using `Equality.copy`
+  + canonical `eclassicType_choiceType` -> instance using `gen_choiceMixin`
+  + definition `porderMixin` and canonical `porderType` -> instance using `isPOrder.Build`
+  + definition `latticeMixin` and canonical `latticeType` -> instance using `POrder_isLattice.Build`
+
+- in `cardinality.v`:
+  + canonical `rat_pointedType` -> instance using `isPointed.Build`
+  + canonical `fimfun_subType` -> instance using `isSub.Build`
+  + definition `fimfuneqMixin` and canonical `fimfuneqType` -> instance using `[Equality of ... by <:]`
+  + definition `fimfunchoiceMixin` and canonical `fimfunchoiceType` -> instance using `[Choice of ... by <:]`
+  + canonicals `fimfun_add`, `fimfun_zmod`, `fimfun_zmodType`, and definition `fimfun_zmodMixin` ->
+    instances using `isZmodClosed.Build` and `[SubChoice_isSubZmodule of ... <:]`
+
+- in `classical_sets.v`:
+  + canonicals
+    `setU_monoid`, `setU_comoid`, `setU_mul_monoid`, `setI_monoid`, `setI_comoid`, `setI_mul_monoid`, `setU_add_monoid`, `setI_add_monoid`
+	-> instances using
+	`isComLaw.Build`, `isMulLaw.Build`, `isComLaw.Build`, `isMulLaw.Build`, `isAddLaw.Build`, `isAddLaw.Build`
+  + module `Pointed` (packed class) -> mixin `isPointed`, structure `Pointed`
+  + canonical `arrow_pointedType` and definition `dep_arrow_pointedType` -> instance using `isPointed.Build`
+  + canonicals
+    `unit_pointedType`, `bool_pointedType`, `Prop_pointedType`, `nat_pointedType`, `prod_pointedType`, `matrix_pointedType`, `option_pointedType`, `pointed_fset`
+	-> instances using
+	`isPointed.Build`
+  + module `Empty` (packed class) -> mixin `isEmpty`, structure `Empty`, factories `Choice_isEmpty`, `Type_isEmpty`
+  + definition `False_emptyMixin` and canonicals `False_eqType`, `False_choiceType`, `False_countType`, `False_finType`, `False_emptyType` -> instance using `Type_isEmpty.Build`
+  + definition `void_emptyMixin` and canonical `void_emptyType` -> instance using `isEmpty.Build`
+  + definition `orderMixin` and canonicals `porderType`, `latticeType`, `distrLatticeType` ->
+    instances using `Choice.copy` and `isMeetJoinDistrLattice.Build`
+  + canonicals `bLatticeType`, `tbLatticeType`, `bDistrLatticeType`, `tbDistrLatticeType` ->
+    instances using `hasBottom.Build` and `hasTop.Build`
+  + canonical `cbDistrLatticeType` -> instance using `hasRelativeComplement.Build`
+  + canonical `ctbDistrLatticeType` -> instance using `hasComplement.Build`
+
+- in `functions.v`:
+  + notation `split`
+  + notation `\_` moved from `fun_scope` to `function_scope`
+  + notations `pinv`, `pPbij`, `pPinj`, `injpPfun`, `funpPinj`
+  + in definition `fct_zmodMixin`: `ZmodMixin` -> `isZmodule.Build`
+  + canonical `fct_zmodType` -> instance using `fct_zmodMixin`
+  + in definition `fct_ringMixin`: `RingMixin` -> `Zmodule_isRing.Build`
+  + canonical `fct_ringType` -> instance using `fct_ringMixin`
+  + canonical `fct_comRingType` ->
+    definition and instance using `Ring_hasCommutativeMul.Build` and `fct_comRingType`
+  + definition `fct_lmodMixin` and canonical `fct_lmodType` ->
+    definition `fct_lmodMixin` and instance using `fct_lmodMixin`
+
 ### Renamed
 
 ### Generalized
@@ -20,6 +76,38 @@
 
 ### Removed
 
+- in `mathcomp_extra.v`:
+  + coercion `choice.Choice.mixin`
+  + lemmas `bigminr_maxr`, definitions `AC_subdef`, `oAC`, `opACE`, canonicals `opAC_law`, `opAC_com_law`
+  + lemmas `some_big_AC`, `big_ACE`, `big_undup_AC`, `perm_big_AC`, `big_const_idem`,
+    `big_id_idem`, `big_mkcond_idem`, `big_split_idem`, `big_id_idem_AC`, `bigID_idem`,
+	`big_rem_AC`, `bigD1_AC`, `sub_big`, `sub_big_seq`, `sub_big_seq_cond`, `uniq_sub_big`,
+	`uniq_sub_big_cond`, `sub_big_idem`, `sub_big_idem_cond`, `sub_in_big`, `le_big_ord`,
+	`subset_big`, `subset_big_cond`, `le_big_nat`, `le_big_ord_cond`
+  + lemmas `bigmax_le`, `bigmax_lt`, `lt_bigmin`, `le_bigmin`
+  + lemmas `bigmax_mkcond`, `bigmax_split`, `bigmax_idl`, `bigmax_idr`, `bigmaxID`
+  + lemmas `sub_bigmax`, `sub_bigmax_seq`, `sub_bigmax_cond`, `sub_in_bigmax`,
+    `le_bigmax_nat`, `le_bigmax_nat_cond`, `le_bigmax_ord`, `le_bigmax_ord_cond`,
+	`subset_bigmax`, `subset_bigmax_cond`
+  + lemmas `bigmaxD1`, `le_bigmax_cond`, `le_bigmax`, `bigmax_sup`, `bigmax_leP`,
+    `bigmax_ltP`, `bigmax_eq_arg`, `eq_bigmax`, `le_bigmax2`
+  + lemmas `bigmin_mkcond`, `bigmin_split`, `bigmin_idl`, `bigmin_idr`, `bigminID`
+  + lemmas `sub_bigmin`, `sub_bigmin_cond`, `sub_bigmin_seq`, `sub_in_bigmin`,
+    `le_bigmin_nat`, `le_bigmin_nat_cond`, `le_bigmin_ord`, `le_bigmin_ord_cond`,
+	`subset_bigmin`, `subset_bigmin_cond`
+  + lemmas `bigminD1`, `bigmin_le_cond`, `bigmin_le`, `bigmin_inf`, `bigmin_geP`,
+    `bigmin_gtP`, `bigmin_eq_arg`, `eq_bigmin`
+
+- in `boolp.v`:
+  + definitions `dep_arrow_eqType`, `dep_arrow_choiceClass`, `dep_arrow_choiceType`
+
+- in `cardinality.v`:
+  + lemma `countable_setT_countMixin`
+
+- in `classical_sets.v`:
+  + notations `PointedType`, `[pointedType of ...]`
+
+
 ### Infrastructure
 
 ### Misc