rocq-prover
diff --git a/‎doc/changelog/01-added/89-Zfloor.rst
-10 b/‎doc/changelog/01-added/89-Zfloor.rst
-10
diff --git a/‎theories/Reals/Reals.v
-1 b/‎theories/Reals/Reals.v
-1
diff --git a/‎theories/Reals/Zfloor.v
-129 b/‎theories/Reals/Zfloor.v
-129
@@ -26,7 +26,6 @@
 
 Require Export Rbase.
 Require Export Rfunctions.
-Require Export Zfloor.
 Require Export SeqSeries.
 Require Export Rtrigo.
 Require Export Ranalysis.