remove unneeded Ndigits dependency

coq-community · Apr 16, 2024 · 49468fc · 49468fc
1 parent bdb702d
commit 49468fc
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 4 deletions.
diff --git a/reals/fast/CRexp.v b/reals/fast/CRexp.v
@@ -36,7 +36,6 @@ Require Import CoRN.reals.fast.CRpower.
 Require Import CoRN.transc.Exponential.
 Require Import CoRN.transc.RealPowers.
 Require Import CoRN.reals.fast.Compress.
-Require Import Coq.NArith.Ndigits.
 Require Import CoRN.reals.fast.ModulusDerivative.
 Require Import CoRN.reals.fast.ContinuousCorrect.
 Require Import CoRN.reals.fast.CRsign.

diff --git a/reals/fast/CRroot.v b/reals/fast/CRroot.v
@@ -33,7 +33,6 @@ Require Import CoRN.model.metric2.Qmetric.
 Require Import Coq.QArith.Qpower.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.reals.fast.Compress.
-Require Import Coq.NArith.Ndigits.
 Require Import CoRN.reals.fast.PowerBound.
 Require Import CoRN.transc.RealPowers.
 Require Import CoRN.reals.fast.ContinuousCorrect.

diff --git a/reals/fast/CRsin.v b/reals/fast/CRsin.v
@@ -39,7 +39,6 @@ Require Import CoRN.reals.fast.ContinuousCorrect.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.transc.PowerSeries.
 Require Import CoRN.transc.SinCos.
-Require Import Coq.NArith.Ndigits.
 Require Import CoRN.reals.fast.Compress.
 Require Import CoRN.reals.fast.PowerBound.
 Require Import CoRN.tactics.CornTac.

diff --git a/reals/fast/PowerBound.v b/reals/fast/PowerBound.v
@@ -22,7 +22,6 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import Coq.NArith.Ndigits.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Program.Basics.
 Require Import Coq.QArith.Qpower.