Split ereal in constructive_ereal and ereal

math-comp · Aug 2, 2022 · 89dc746 · 89dc746
1 parent 0b421c7
commit 89dc746
Show file tree

Hide file tree

Showing 4 changed files with 3,414 additions and 3,347 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/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)
diff --git a/_CoqProject b/_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