diff --git a/tests/numbers.ref b/tests/numbers.ref new file mode 100644 index 0000000000000000000000000000000000000000..8dd3efde5e3054ef29120bf0d328c4753761f23b --- /dev/null +++ b/tests/numbers.ref @@ -0,0 +1,8 @@ +le + : nat → nat → Prop +le + : nat → nat → Prop +le + : nat → nat → Prop +le + : nat → nat → Prop diff --git a/tests/numbers.v b/tests/numbers.v new file mode 100644 index 0000000000000000000000000000000000000000..3c8676c9c2369859501ce054d210f0359adbe85f --- /dev/null +++ b/tests/numbers.v @@ -0,0 +1,22 @@ +From stdpp Require base numbers prelude. + +(** Check that we always get the [le] function on [nat]. *) +Module test1. + Import stdpp.base. + Check le. +End test1. + +Module test2. + Import stdpp.prelude. + Check le. +End test2. + +Module test3. + Import stdpp.numbers. + Check le. +End test3. + +Module test4. + Import stdpp.list. + Check le. +End test4. diff --git a/theories/base.v b/theories/base.v index 7d63f1249391776006db679758172c8fd4b09307..a4cfdfb32ad72b913dae2f8b6ed1f556cf72e9f2 100644 --- a/theories/base.v +++ b/theories/base.v @@ -3,7 +3,7 @@ that are used throughout the whole development. Most importantly it contains abstract interfaces for ordered structures, sets, and various other data structures. *) -From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid. +From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Arith. From Coq Require Import Permutation. Set Default Proof Using "Type". Export ListNotations. diff --git a/theories/numbers.v b/theories/numbers.v index d0b9d29d04566e1fda5cbc394844599dd5177f93..384977883ae3cd74afa07531bf99d0f6581f414b 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -1,7 +1,7 @@ (** This file collects some trivial facts on the Coq types [nat] and [N] for natural numbers, and the type [Z] for integers. It also declares some useful notations. *) -From Coq Require Export EqdepFacts PArith NArith ZArith NPeano. +From Coq Require Export EqdepFacts PArith NArith ZArith Arith. From Coq Require Import QArith Qcanon. From stdpp Require Export base decidable option. Set Default Proof Using "Type".