fix changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -71,11 +71,6 @@
            `derivable_oy_continuousW`,
            `derivable_Nyo_continuousWoo`,
            `derivable_Nyo_continuousW`
-- in `probability.v`:
-  + lemmas `eq_bernoulli`, `eq_bernoulliV2`
-
-- file `mathcomp_extra.v`
-  + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat`
 
 - in `measurable_function.v`:
   + lemma `preimage_set_system_compS`
@@ -376,19 +371,7 @@
   + `le_ereal_inf` -> `ereal_inf_le_tmp`
   + `lb_ereal_inf` -> `le_ereal_inf_tmp`
   + `ereal_sup_ge` -> `le_ereal_sup_tmp`
-- in `kernel.v`:
-  + `isFiniteTransition` -> `isFiniteTransitionKernel`
-- in `lebesgue_integral.v`:
-  + `fubini1a` -> `integrable12ltyP`
-  + `fubini1b` -> `integrable21ltyP`
-  + `measurable_funP` -> `measurable_funPT` (field of `isMeasurableFun` mixin)
-
-- in `mathcomp_extra.v`
-  + `comparable_min_le_min` -> `comparable_le_min2`
-  + `comparable_max_le_max` -> `comparable_le_max2`
-  + `min_le_min` -> `le_min2`
-  + `max_le_max` -> `le_max2`
-  + `real_sqrtC` -> `sqrtC_real`
+
 - in `measure.v`
   + `preimage_class` -> `preimage_set_system`
   + `image_class` -> `image_set_system`
@@ -401,26 +384,9 @@
 
 ### Renamed
 
-- in `lebesgue_measure.v`:
-  + `measurable_fun_indic` -> `measurable_indic`
-  + `emeasurable_fun_sum` -> `emeasurable_sum`
-  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
-  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
 - in `probability.v`:
   + `expectationM` -> `expectationZl`
 
-- in `classical_sets.v`:
-  + `preimage_itv_o_infty` -> `preimage_itvoy`
-  + `preimage_itv_c_infty` -> `preimage_itvcy`
-  + `preimage_itv_infty_o` -> `preimage_itvNyo`
-  + `preimage_itv_infty_c` -> `preimage_itvNyc`
-
-- in `constructive_ereal.v`:
-  + `maxeMr` -> `maxe_pMr`
-  + `maxeMl` -> `maxe_pMl`
-  + `mineMr` -> `mine_pMr`
-  + `mineMl` -> `mine_pMl`
-
 - in `probability.v`:
   + `integral_distribution` -> `ge0_integral_distribution`
 
@@ -472,45 +438,6 @@
 
 - in `ereal.v`:
   + notation `ereal_sup_le` (was deprecated since 1.11.0)
-- file `mathcomp_extra.v`
-  + lemma `Pos_to_natE` (moved to `Rstruct.v`)
-  + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v`
-    since MathComp 2.1.0)
-- in `sequences.v`:
-  + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
-    `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
-- in `topology_structure.v`:
-  + lemma `closureC`
-
-- in file `lebesgue_integral.v`:
-  + lemma `approximation`
-
-### Removed
-
-- in `lebesgue_integral.v`:
-  + definition `cst_mfun`
-  + lemma `mfun_cst`
-
-- in `cardinality.v`:
-  + lemma `cst_fimfun_subproof`
-
-- in `lebesgue_integral.v`:
-  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
-  + lemma `cst_nnfun_subproof` (turned into a `Let`)
-  + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
-
-- in `lebesgue_integral.v`:
-  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
-  + notation `measurable_fun_indic` (deprecation since 0.6.3)
-- in `constructive_ereal.v`
-  + notation `lee_opp` (deprecated since 0.6.5)
-  + notation `lte_opp` (deprecated since 0.6.5)
-- in `measure.v`:
-  + `dynkin_setI_bigsetI` (use `big_ind` instead)
-
-- in `lebesgue_measurable.v`:
-  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
-  + notation `measurable_power_pos` (deprecated since 0.6.4)
 
 ### Infrastructure
 

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Coq Require Setoid.
+From Corelib Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

reals/reals.v

@@ -43,7 +43,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.