Move Qreals from QArith to Reals

coq · proux01 · Feb 3, 2025 · Dec 17, 2023 · Dec 14, 2023 · Dec 14, 2023
commit 7c873290133f44e9ea8268aef0d496f145ef4bce
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
@@ -174,7 +174,6 @@ The standard library is composed of the following subdirectories:</p>
     theories/QArith/Qring.v
     theories/QArith/Qfield.v
     (theories/QArith/QArith.v)
-    theories/QArith/Qreals.v
     theories/QArith/Qcanon.v
     theories/QArith/Qcabs.v
     theories/QArith/Qround.v
@@ -570,6 +569,7 @@ The standard library is composed of the following subdirectories:</p>
     theories/Reals/Cauchy/ConstructiveCauchyReals.v
     theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
     theories/Reals/Cauchy/ConstructiveCauchyAbs.v
+    theories/Reals/Qreals.v
   </dd>
 
   </dl>

diff --git a/theories/QArith/Qreals.v → theories/Reals/Qreals.v b/theories/QArith/Qreals.v → theories/Reals/Qreals.v