Split ereal in constructive_ereal and ereal

Author: proux01

CHANGELOG_UNRELEASED.md

@@ -104,3 +104,7 @@
 ### Infrastructure
 
 ### Misc
+
+- file `ereal.v` split in two files `constructive_ereal.v` and
+  `ereal.v` (the latter exports the former, so the "Require Import
+  ereal" can just be kept unchanged)

_CoqProject

@@ -8,6 +8,7 @@
 
 theories/mathcomp_extra.v
 theories/boolp.v
+theories/constructive_ereal.v
 theories/ereal.v
 theories/reals.v
 theories/landau.v