R^o type constraints in ln_concave

CHANGELOG_UNRELEASED.md

@@ -59,6 +59,9 @@
 - in `constructive_ereal.v`:
   + lemmas `expe_ge0`, `expe_eq0`, `expe_gt0`
 
+- in `convex.v`:
+  + `convType` on `realDomainType`, `realFieldType` and `realType`
+
 ### Changed
 
 - in `pi_irrational`:
@@ -115,6 +118,8 @@
   + notation `measurable_fun_ext` (deprecated since 0.6.2)
   + notations `measurable_fun_id`, `measurable_fun_cst`, `measurable_fun_comp` (deprecated since 0.6.3)
   + notation `measurable_funT_comp` (deprecated since 0.6.3)
+- in `convex.v`:
+  + instance of `convType` for `R^o` with `R : realDomainType`
 
 ### Infrastructure
 

_CoqProject

@@ -30,7 +30,6 @@ reals/constructive_ereal.v
 reals/reals.v
 reals/real_interval.v
 reals/signed.v
-reals/interval_inference.v
 reals/prodnormedzmodule.v
 reals/all_reals.v
 experimental_reals/xfinmap.v

reals/all_reals.v

@@ -1,4 +1,3 @@
-From mathcomp Require Export interval_inference.
 From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export reals.
 From mathcomp Require Export real_interval.