changelog up to convex.v

CHANGELOG_UNRELEASED.md

@@ -5,11 +5,18 @@
 ### Added
 
 - in `cantor.v`:
-  + definitions `pointed_principal_filter`,
-    `pointed_discrete_topology`
+  + definition `pointed_principal_filter`, instances using `Pointed.on` and `hasNbhs.Build`
+  + definition `pointed_discrete_topology`
   + lemma `discrete_pointed`
   + lemma `discrete_bool_compact`
 
+- in `charge.v`:
+  + `cscale` instances using `SigmaFinite_isFinite.Build` and `isAdditiveCharge.Build`
+
+- in `convex.v`:
+  + definition `convex_lmodType` with instances using `Choice.on` and `isConvexSpace.Build`
+  + definition `convex_realDomainType` with instance using `isConvexSpace.Build`
+
 ### Changed
 
 - in `boolp.v`:
@@ -68,10 +75,60 @@
   + definition `fct_lmodMixin` and canonical `fct_lmodType` ->
     definition `fct_lmodMixin` and instance using `fct_lmodMixin`
 
+- in `Rstruct.v`:
+  + canonicals `R_eqMixin`, `R_eqType` -> instance using `hasDecEq.Build`
+  + definition `R_choiceMixin` and canonical `R_choiceType` -> instance using `hasChoice.Build`
+  + definition `R_zmodMixin` and canonical `R_zmodType` -> instance using `isZmodule.Build`
+  + definition `R_ringMixin` and canonicals `R_ringType`, `R_comRingType` ->
+    instances using `Zmodule_isRing.Build`, `Ring_hasCommutativeMul.Build`
+  + canonicals `Radd_monoid`, `Radd_comoid` -> instance using `isComLaw.Build`
+  + canonicals `Rmul_monoid`, `Rmul_comoid` -> instance using `isComLaw.Build`
+  + canonical `Rmul_mul_law` -> instance using `isMulLaw.Build`
+  + canonical `Radd_add_law` -> instance using `isAddLaw.Build`
+  + definition `R_unitRingMixin` and canonical `R_unitRing` -> instance using `Ring_hasMulInverse.Build`
+  + canonicals `R_comUnitRingType` and `R_idomainType` ->
+    instance using `ComUnitRing_isIntegral.Build`
+  + in lemma `R_fieldMixin`: `GRing.Field.mixin_of` -> `GRing.field_axiom`
+  + definition `Definition` and canonical `R_fieldType` -> instance using `UnitRing_isField.Build`
+  + definition `R_numMixin`, canonicals `R_porderType`, `R_numDomainType`, `R_normedZmodType`, `R_numFieldType`
+    ->
+	instance using `IntegralDomain_isNumRing.Build`
+  + in lemma `R_total`: `totalPOrderMixin` -> `total`
+  + canonicals `R_latticeType`, `R_distrLatticeType`, `R_orderType`, `R_realDomainType`, `R_realFieldType`
+    -> instance using `POrder_isTotal.Build`
+  + in lemmas `Rarchimedean_axiom`, `Rreal_closed_axiom`: `R_numDomainType` -> `[the numDomainType of R : Type]`
+  + canonical `R_realArchiFieldType` -> instance using `RealField_isArchimedean.Build`
+  + canonical `R_rcfType` -> instance using `RealField_isClosed.Build`
+  + definition `real_realMixin` and canonical `real_realType` -> instance using `ArchimedeanField_isReal.Build`
+  + canonicals `R_pointedType`, `R_filteredType`, `R_topologicalType`, `R_uniformType`,
+    `R_pseudoMetricType` -> instance using `PseudoMetric.copy`
+
+- in `altreals/discrete.v`:
+  + canonical `pred_sub_subTypeP` -> instance using `[isSub for ...]`
+  + definition `pred_sub_eqMixin` and canonical `pred_sub_eqType` ->
+    instance using `[Equality of ... by <:]`
+  + definition `pred_sub_choiceMixin` and canonical `pred_sub_choiceType` ->
+    instance using `[Choice of ... <:]`
+  + definition `pred_sub_countMixin` and `pred_sub_countType` ->
+    instance using `[Countable of ... by <:]`
+  + definitions `countable_countMixin` and `countable_countType` -> `countable_countMixin`
+  + definitions `countable_choiceMixin` and `countable_choiceType` -> `countable_choiceMixin`
+
+- in `altreals/xfinmap.v`:
+  + in lemmas `enum_fset0` and `enum_fset1`: notation `[fintype of ...]` -> type constraint `... : finType`
+
+- in `cantor.v`:
+	+ in definition `tree_of` and lemma `cantor_like_finite_prod`:
+	  `pointed_discrete` -> `pointed_discrete_topology`
+
 ### Renamed
 
 ### Generalized
 
+- in `cantor.v`:
+  + in definition `cantor_space`: `product_uniformType` -> `prod_topology`
+	* instances using `Pointed.on`, `Nbhs.on`, `Topological.on`
+
 ### Deprecated
 
 ### Removed
@@ -107,6 +164,14 @@
 - in `classical_sets.v`:
   + notations `PointedType`, `[pointedType of ...]`
 
+- in `altreals/discrete.v`:
+  + notation `[countable of ...]`
+
+- in `cantor.v`:
+  + definition `pointed_discrete`
+
+- in `convex.v`:
+  + field `convexspacechoiceclass`, canonicals `conv_eqType`, `conv_choiceType`, `conv_choiceType`
 
 ### Infrastructure