Skip to content
Snippets Groups Projects
Commit f7ea3065 authored by Pierre Rousselin's avatar Pierre Rousselin
Browse files

Remove reference to NPeano

parent 8c98553a
No related branches found
No related tags found
1 merge request!535Remove Import NPeano
...@@ -21,7 +21,7 @@ The results for [Qc] are not yet in a module. This is in part because they ...@@ -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 still follow the old/non-module style in Coq's standard library. See also
https://gitlab.mpi-sws.org/iris/stdpp/-/issues/147. *) 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 Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option. From stdpp Require Export base decidable option.
From stdpp Require Import well_founded. From stdpp Require Import well_founded.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment