Split ereal in ereal and classical_ereal

Author: proux01

CHANGELOG_UNRELEASED.md

@@ -137,4 +137,8 @@
 
 ### Infrastructure
 
-### Misc
+### Misc
+
+- file `ereal.v` split in two files `ereal.v` and `classical_ereal.v`
+  (the latter exports the former, so the "Require Import ereal"
+  can just be replaced by "Require Import classical_ereal")

_CoqProject

@@ -10,6 +10,7 @@
 theories/mathcomp_extra.v
 theories/boolp.v
 theories/ereal.v
+theories/classical_ereal.v
 theories/reals.v
 theories/landau.v
 theories/classical_sets.v