diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3ac6cb1aa..cc4f017dd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,155 @@
 # Changelog
 
-Last releases: [[0.3.7] - 2021-04-01](#037---2021-04-01) and [[0.3.6] - 2021-03-04](#036---2021-03-04)
+Last releases: [[0.3.8] - 2021-06-01](#038---2021-06-01) and [[0.3.7] - 2021-04-01](#037---2021-04-01)
+
+## [0.3.8] - 2021-06-01
+
+### Added
+
+- file `reals.v`:
+  + lemmas `le_floor`, `le_ceil`
+- in `ereal.v`:
+  + lemmas `big_nat_widenl`, `big_geq_mkord`
+  + lemmas `lee_sum_nneg_natr`, `lee_sum_nneg_natl`
+  + lemmas `ereal_sup_gt`, `ereal_inf_lt`
+  + notation `0`/`1` for `0%R%:E`/`1%R:%E` in `ereal_scope`
+- in `classical_sets.v`
+  + lemma `subset_bigsetU_cond`
+  + lemma `eq_imagel`
+- in `sequences.v`:
+  + notations `\sum_(i <oo) F i`
+  + lemmas `ereal_pseries_sum_nat`, `lte_lim`
+  + lemmas `is_cvg_ereal_nneg_natsum_cond`, `is_cvg_ereal_nneg_natsum`
+  + lemma `ereal_pseriesD`, `ereal_pseries0`, `eq_ereal_pseries`
+  + lemmas `leq_fact`, `prod_rev`, `fact_split`
+  + definition `exp_coeff`
+  + lemmas `exp_coeff_ge0`, `series_exp_coeff0`, `is_cvg_series_exp_coeff_pos`,
+    ` normed_series_exp_coeff`, `is_cvg_series_exp_coeff `, `cvg_exp_coeff`
+  + definition `expR`
+- in `measure.v`:
+  + lemma `eq_bigcupB_of_bigsetU`
+  + definitions `caratheodory_type`
+  + definition `caratheodory_measure` and lemma `caratheodory_measure_complete`
+  + internal definitions and lemmas that may be deprecated and hidden in the future:
+    * `caratheodory_measurable`, notation `... .-measurable`,
+    * `le_caratheodory_measurable`, `outer_measure_bigcup_lim`,
+      `caratheodory_measurable_{set0,setC,setU_le,setU,bigsetU,setI,setD}`
+      `disjoint_caratheodoryIU`, `caratheodory_additive`,
+          `caratheodory_lim_lee`, `caratheodory_measurable_trivIset_bigcup`,
+      `caratheodory_measurable_bigcup`
+  + definition `measure_is_complete`
+- file `csum.v`:
+  + lemmas `ereal_pseries_pred0`, `ub_ereal_sup_adherent_img`
+  + definition `fsets`, lemmas `fsets_set0`, `fsets_self`, `fsetsP`, `fsets_img`
+  + definition `fsets_ord`, lemmas `fsets_ord_nat`, `fsets_ord_subset`
+  + definition `csum`, lemmas `csum0`, `csumE`, `csum_ge0`, `csum_fset`
+    `csum_image`, `ereal_pseries_csum`, `csum_bigcup`
+  + notation `\csum_(i in S) a i`
+- file `cardinality.v`
+  + lemmas `in_inj_comp`, `enum0`, `enum_recr`, `eq_set0_nil`, `eq_set0_fset0`,
+    `image_nat_maximum`, `fset_nat_maximum`
+  + defintion `surjective`, lemmas `surjective_id`, `surjective_set0`,
+    `surjective_image`, `surjective_image_eq0`, `surjective_comp`
+  + definition `set_bijective`,
+  + lemmas `inj_of_bij`, `sur_of_bij`, `set_bijective1`, `set_bijective_image`,
+    `set_bijective_subset`, `set_bijective_comp`
+  + definition `inverse`
+  + lemmas `injective_left_inverse`, `injective_right_inverse`,
+    `surjective_right_inverse`,
+  + notation `` `I_n ``
+  + lemmas `II0`, `II1`, `IIn_eq0`, `II_recr`
+  + lemmas `set_bijective_D1`, `pigeonhole`, `Cantor_Bernstein`
+  + definition `card_le`, notation `_ #<= _`
+  + lemmas `card_le_surj`, `surj_card_le`, `card_lexx`, `card_le0x`,
+    `card_le_trans`, `card_le0P`, `card_le_II`
+  + definition `card_eq`, notation `_ #= _`
+  + lemmas `card_eq_sym`, `card_eq_trans`, `card_eq00`, `card_eqP`, `card_eqTT`,
+    `card_eq_II`, `card_eq_le`, `card_eq_ge`, `card_leP`
+  + lemma `set_bijective_inverse`
+  + definition `countable`
+  + lemmas `countable0`, `countable_injective`, `countable_trans`
+  + definition `set_finite`
+  + lemmas `set_finiteP`, `set_finite_seq`, `set_finite_countable`, `set_finite0`
+  + lemma `set_finite_bijective`
+  + lemmas `subset_set_finite`, `subset_card_le`
+  + lemmas `injective_set_finite`, `injective_card_le`, `set_finite_preimage`
+  + lemmas `surjective_set_finite`, `surjective_card_le`
+  + lemmas `set_finite_diff`, `card_le_diff`
+  + lemmas `set_finite_inter_set0_union`, `set_finite_inter`
+  + lemmas `ex_in_D`, definitions `min_of_D`, `min_of_D_seq`, `infsub_enum`, lemmas
+    `min_of_D_seqE`, `increasing_infsub_enum`, `sorted_infsub_enum`,
+   `injective_infsub_enum`, `subset_infsub_enum`, `infinite_nat_subset_countable`
+  + definition `enumeration`, lemmas `enumeration_id`, `enumeration_set0`.
+  + lemma `ex_enum_notin`, definitions `min_of`, `minf_of_e_seq`, `smallest_of`
+  + definition `enum_wo_rep`, lemmas `enum_wo_repE`, `min_of_e_seqE`,
+    `smallest_of_e_notin_enum_wo_rep`, `injective_enum_wo_rep`, `surjective_enum_wo_rep`,
+    `set_bijective_enum_wo_rep`, `enumration_enum_wo_rep`, `countable_enumeration`
+  + lemmas `infinite_nat`, `infinite_prod_nat`, `countable_prod_nat`,
+    `countably_infinite_prod_nat`
+
+### Changed
+
+- in `classical_sets.v`, lemma `subset_bigsetU`
+- in `ereal.v`:
+  + change implicits of lemma `lee_sum_nneg_ord`
+  + `ereal_sup_ninfty` and `ereal_inf_pinfty` made equivalences
+  + change the notation `{ereal R}` to `\bar R` and attach it to the scope `ereal_scope`
+  + argument of `%:E` in `%R` by default
+  + `F` argument of `\sum` in `%E` by default
+- in `topology.v`:
+  + change implicits of lemma `cvg_app`
+- in `normedtype.v`:
+  + `coord_continuous` generalized
+- in `sequences.v`:
+  + change implicits of lemma `is_cvg_ereal_nneg_series`
+  + statements changed from using sum of ordinals to sum of nats
+    * definition `series`
+    * lemmas `ereal_nondecreasing_series`, `ereal_nneg_series_lim_ge`
+    * lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series`
+    * lemmas `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty`
+
+### Renamed
+
+- in `ereal.v`:
+  + `er` -> `extended`
+  + `ERFin` -> `EFin`
+  + `ERPInf` -> `EPInf`
+  + `ERNInf` -> `ENInf`
+  + `real_of_er` -> `real_of_extended`
+  + `real_of_erD` -> `real_of_extendedD`
+  + `ERFin_real_of_er` -> `EFin_real_of_extended`
+  + `real_of_er_expand` -> `real_of_extended_expand`
+  + `NERFin` -> `NEFin`
+  + `addERFin` -> `addEFin`
+  + `sumERFin`-> `sumEFin`
+  + `subERFin` -> `subEFin`
+- in `reals.v`:
+  + `ler_ceil` -> `ceil_ge`
+  + `Rceil_le` -> `le_Rceil`
+  + `le_Rceil` -> `Rceil_ge`
+  + `ge_Rfloor` -> `Rfloor_le`
+  + `ler_floor` -> `floor_le`
+  + `Rfloor_le` -> `le_Rfloor`
+- in `topology.v`:
+  + lemmas `onT_can` -> `onS_can`,
+    `onT_can_in` -> `onS_can_in`,
+    `in_onT_can` -> ``in_onS_can`
+    (now in MathComp)
+- in `sequences,v`:
+  + `is_cvg_ereal_nneg_series_cond`
+- in `forms.v`:
+  + `symmetric` -> `symmetric_form`
+
+### Removed
+
+- in `classical_sets.v`
+  + lemmas `eq_set_inl`, `set_in_in`
+- from `topology.v`:
+  + lemmas `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`,
+    `monoRL_in`, `can_mono_in`, `onW_can`, `onW_can_in`, `in_onW_can`,
+    `onT_can`, `onT_can_in`, `in_onT_can` (now in MathComp)
+- in `forms.v`:
+  + lemma `mxdirect_delta`, `row_mx_eq0`, `col_mx_eq0`, `map_mx_comp`
 
 ## [0.3.7] - 2021-04-01
 
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 14136cdff..c1ee5bdc8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -3,158 +3,13 @@
 ## [Unreleased]
 
 ### Added
- 
-- in `ereal.v`:
-  + lemmas `big_nat_widenl`, `big_geq_mkord`
-  + lemmas `lee_sum_nneg_natr`, `lee_sum_nneg_natl`
-  + lemmas `ereal_sup_gt`, `ereal_inf_lt`
-- in `sequences.v`:
-  + notations `\sum_(i <oo) F i`
-  + lemmas `ereal_pseries_sum_nat`, `lte_lim`
-  + lemmas `is_cvg_ereal_nneg_natsum_cond`, `is_cvg_ereal_nneg_natsum`
-  + lemma `ereal_pseriesD`, `ereal_pseries0`, `eq_ereal_pseries`
-- in `classical_sets.v`
-  + lemma `subset_bigsetU_cond`
-  + lemma `eq_imagel`
-- in `measure.v`:
-  + lemma `eq_bigcupB_of_bigsetU`
-  + definitions `caratheodory_type`
-  + definition `caratheodory_measure` and lemma `caratheodory_measure_complete`
-  + internal definitions and lemmas that may be deprecated and hidden in the future:
-    * `caratheodory_measurable`, notation `... .-measurable`,
-    * `le_caratheodory_measurable`, `outer_measure_bigcup_lim`,
-      `caratheodory_measurable_{set0,setC,setU_le,setU,bigsetU,setI,setD}`
-      `disjoint_caratheodoryIU`, `caratheodory_additive`,
-          `caratheodory_lim_lee`, `caratheodory_measurable_trivIset_bigcup`,
-      `caratheodory_measurable_bigcup`
-- file `csum.v`:
-  + lemmas `ereal_pseries_pred0`, `ub_ereal_sup_adherent_img`
-  + definition `fsets`, lemmas `fsets_set0`, `fsets_self`, `fsetsP`, `fsets_img`
-  + definition `fsets_ord`, lemmas `fsets_ord_nat`, `fsets_ord_subset`
-  + definition `csum`, lemmas `csum0`, `csumE`, `csum_ge0`, `csum_fset`
-    `csum_image`, `ereal_pseries_csum`, `csum_bigcup`
-  + notation `\csum_(i in S) a i`
-- file `cardinality.v`
-  + lemmas `in_inj_comp`, `enum0`, `enum_recr`, `eq_set0_nil`, `eq_set0_fset0`,
-    `image_nat_maximum`, `fset_nat_maximum`
-  + defintion `surjective`, lemmas `surjective_id`, `surjective_set0`,
-    `surjective_image`, `surjective_image_eq0`, `surjective_comp`
-  + definition `set_bijective`,
-  + lemmas `inj_of_bij`, `sur_of_bij`, `set_bijective1`, `set_bijective_image`,
-    `set_bijective_subset`, `set_bijective_comp`
-  + definition `inverse`
-  + lemmas `injective_left_inverse`, `injective_right_inverse`,
-    `surjective_right_inverse`,
-  + notation `` `I_n ``
-  + lemmas `II0`, `II1`, `IIn_eq0`, `II_recr`
-  + lemmas `set_bijective_D1`, `pigeonhole`, `Cantor_Bernstein`
-  + definition `card_le`, notation `_ #<= _`
-  + lemmas `card_le_surj`, `surj_card_le`, `card_lexx`, `card_le0x`,
-    `card_le_trans`, `card_le0P`, `card_le_II`
-  + definition `card_eq`, notation `_ #= _`
-  + lemmas `card_eq_sym`, `card_eq_trans`, `card_eq00`, `card_eqP`, `card_eqTT`,
-    `card_eq_II`, `card_eq_le`, `card_eq_ge`, `card_leP`
-  + lemma `set_bijective_inverse`
-  + definition `countable`
-  + lemmas `countable0`, `countable_injective`, `countable_trans`
-  + definition `set_finite`
-  + lemmas `set_finiteP`, `set_finite_seq`, `set_finite_countable`, `set_finite0`
-  + lemma `set_finite_bijective`
-  + lemmas `subset_set_finite`, `subset_card_le`
-  + lemmas `injective_set_finite`, `injective_card_le`, `set_finite_preimage`
-  + lemmas `surjective_set_finite`, `surjective_card_le`
-  + lemmas `set_finite_diff`, `card_le_diff`
-  + lemmas `set_finite_inter_set0_union`, `set_finite_inter`
-  + lemmas `ex_in_D`, definitions `min_of_D`, `min_of_D_seq`, `infsub_enum`, lemmas
-    `min_of_D_seqE`, `increasing_infsub_enum`, `sorted_infsub_enum`,
-   `injective_infsub_enum`, `subset_infsub_enum`, `infinite_nat_subset_countable`
-  + definition `enumeration`, lemmas `enumeration_id`, `enumeration_set0`.
-  + lemma `ex_enum_notin`, definitions `min_of`, `minf_of_e_seq`, `smallest_of`
-  + definition `enum_wo_rep`, lemmas `enum_wo_repE`, `min_of_e_seqE`,
-    `smallest_of_e_notin_enum_wo_rep`, `injective_enum_wo_rep`, `surjective_enum_wo_rep`,
-    `set_bijective_enum_wo_rep`, `enumration_enum_wo_rep`, `countable_enumeration`
-  + lemmas `infinite_nat`, `infinite_prod_nat`, `countable_prod_nat`,
-    `countably_infinite_prod_nat`
-- in `measure.v`:
-  + definition `measure_is_complete`
-- in `ereal.v`:
-  + notation `0`/`1` for `0%R%:E`/`1%R:%E` in `ereal_scope`
-- file `reals.v`:
-  + lemmas `le_floor`, `le_ceil`
-- in `sequences,v`:
-  + lemmas `leq_fact`, `prod_rev`, `fact_split`
-  + definition `exp_coeff`
-  + lemmas `exp_coeff_ge0`, `series_exp_coeff0`, `is_cvg_series_exp_coeff_pos`,
-    ` normed_series_exp_coeff`, `is_cvg_series_exp_coeff `, `cvg_exp_coeff`
-  + definition `expR`
 
 ### Changed
 
-- in `ereal.v`:
-  + change implicits of lemma `lee_sum_nneg_ord`
-  + `ereal_sup_ninfty` and `ereal_inf_pinfty` made equivalences
-- in `sequences.v`:
-  + change implicits of lemma `is_cvg_ereal_nneg_series`
-  + statements changed from using sum of ordinals to sum of nats
-    * definition `series`
-    * lemmas `ereal_nondecreasing_series`, `ereal_nneg_series_lim_ge`
-    * lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series`
-    * lemmas `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty`
-- in `classical_sets.v`, lemma `subset_bigsetU`
-- in `ereal.v`:
-  + change the notation `{ereal R}` to `\bar R` and attach it to the scope `ereal_scope`
-- in `topology.v`:
-  + change implicits of lemma `cvg_app`
-
-- in `ereal.v`:
-  + argument of `%:E` in `%R` by default
-  + `F` argument of `\sum` in `%E` by default
-- in `normedtype.v`:
-  + `coord_continuous` generalized
-
 ### Renamed
 
-- in `sequences,v`:
-  + `is_cvg_ereal_nneg_series_cond`
-- in `topology.v`:
-  + lemmas `onT_can` -> `onS_can`,
-    `onT_can_in` -> `onS_can_in`,
-    `in_onT_can` -> ``in_onS_can`
-    (now in MathComp)
-- in `ereal.v`:
-  + `er` -> `extended`
-  + `ERFin` -> `EFin`
-  + `ERPInf` -> `EPInf`
-  + `ERNInf` -> `ENInf`
-  + `real_of_er` -> `real_of_extended`
-  + `real_of_erD` -> `real_of_extendedD`
-  + `ERFin_real_of_er` -> `EFin_real_of_extended`
-  + `real_of_er_expand` -> `real_of_extended_expand`
-  + `NERFin` -> `NEFin`
-  + `addERFin` -> `addEFin`
-  + `sumERFin`-> `sumEFin`
-  + `subERFin` -> `subEFin`
-- in `reals.v`:
-  + `ler_ceil` -> `ceil_ge`
-  + `Rceil_le` -> `le_Rceil`
-  + `le_Rceil` -> `Rceil_ge`
-  + `ge_Rfloor` -> `Rfloor_le`
-  + `ler_floor` -> `floor_le`
-  + `Rfloor_le` -> `le_Rfloor`
-- in `forms.v`:
-  + `symmetric` -> `symmetric_form`
-
 ### Removed
 
-- in `classical_sets.v`
-  + lemmas `eq_set_inl`, `set_in_in`
-- from `topology.v`:
-  + lemmas `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`,
-    `monoRL_in`, `can_mono_in`, `onW_can`, `onW_can_in`, `in_onW_can`,
-    `onT_can`, `onT_can_in`, `in_onT_can` (now in MathComp)
-- in `forms.v`:
-  + lemma `mxdirect_delta`, `row_mx_eq0`, `col_mx_eq0`, `map_mx_comp`
-
 ### Infrastructure
 
 ### Misc
diff --git a/INSTALL.md b/INSTALL.md
index ae56a135f..4a33162a7 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.7
+$ opam install coq-mathcomp-analysis.0.3.8
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
diff --git a/README.md b/README.md
index f0c5edcf5..661b5adfc 100644
--- a/README.md
+++ b/README.md
@@ -26,8 +26,10 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Marie Kerjean
   - Assia Mahboubi (initial)
   - Damien Rouhling (initial)
+  - Pierre Roux
   - Kazuhiko Sakaguchi
   - Pierre-Yves Strub (initial)
+  - Laurent Thery
 - License: [CeCILL-C](LICENSE)
 - Compatible Coq versions: Coq 8.11 to 8.13 (or dev)
 - Additional dependencies:
diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
index b5262433a..45fddae68 100644
--- a/coq-mathcomp-analysis.opam
+++ b/coq-mathcomp-analysis.opam
@@ -40,6 +40,8 @@ authors: [
   "Marie Kerjean"
   "Assia Mahboubi"
   "Damien Rouhling"
+  "Pierre Roux"
   "Kazuhiko Sakaguchi"
   "Pierre-Yves Strub"
+  "Laurent Thery"
 ]
diff --git a/meta.yml b/meta.yml
index fd3447898..baba48a06 100644
--- a/meta.yml
+++ b/meta.yml
@@ -25,10 +25,14 @@ authors:
   initial: true
 - name: Damien Rouhling
   initial: true
+- name: Pierre Roux
+  initial: false
 - name: Kazuhiko Sakaguchi
   initial: false
 - name: Pierre-Yves Strub
   initial: true
+- name: Laurent Thery
+  initial: false
 
 opam-file-maintainer: Reynald Affeldt <reynald.affeldt@aist.go.jp>