diff --git a/stdpp/numbers.v b/stdpp/numbers.v index 34cb6450debaf6d4e5d92a4e792b68ef11ce7b39..90a94f0191e1a6084f352c864fc7e5063a127b10 100644 --- a/stdpp/numbers.v +++ b/stdpp/numbers.v @@ -21,7 +21,7 @@ The results for [Qc] are not yet in a module. This is in part because they still follow the old/non-module style in Coq's standard library. See also https://gitlab.mpi-sws.org/iris/stdpp/-/issues/147. *) -From Coq Require Export EqdepFacts PArith NArith ZArith NPeano. +From Coq Require Export EqdepFacts PArith NArith ZArith. From Coq Require Import QArith Qcanon. From stdpp Require Export base decidable option. From stdpp Require Import well_founded.