From 964ea47bb843d0555fe7cc2fa0d0f35f8b4a4332 Mon Sep 17 00:00:00 2001
From: Olivier Laurent <olivier.laurent@ens-lyon.fr>
Date: Thu, 7 May 2020 09:30:48 +0200
Subject: [PATCH] overlay for coq/coq#12162

---
 tests/numbers.ref | 16 ++++++++++++++++
 tests/numbers.v   | 26 ++++++++++++++++++++++++++
 theories/base.v   |  5 ++++-
 3 files changed, 46 insertions(+), 1 deletion(-)
 create mode 100644 tests/numbers.ref
 create mode 100644 tests/numbers.v

diff --git a/tests/numbers.ref b/tests/numbers.ref
new file mode 100644
index 00000000..05fcae6e
--- /dev/null
+++ b/tests/numbers.ref
@@ -0,0 +1,16 @@
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
diff --git a/tests/numbers.v b/tests/numbers.v
new file mode 100644
index 00000000..0b0c6d01
--- /dev/null
+++ b/tests/numbers.v
@@ -0,0 +1,26 @@
+From stdpp Require base numbers prelude.
+
+(** Check that we always get the [le] and [lt] functions on [nat]. *)
+Module test1.
+  Import stdpp.base.
+  Check le.
+  Check lt.
+End test1.
+
+Module test2.
+  Import stdpp.prelude.
+  Check le.
+  Check lt.
+End test2.
+
+Module test3.
+  Import stdpp.numbers.
+  Check le.
+  Check lt.
+End test3.
+
+Module test4.
+  Import stdpp.list.
+  Check le.
+  Check lt.
+End test4.
diff --git a/theories/base.v b/theories/base.v
index 7d63f124..538dd416 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -3,7 +3,10 @@ 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.
+(* We want to ensure that [le] and [lt] refer to operations on [nat].
+These two functions being defined both in [Coq.Bool] and in [Coq.Peano],
+we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Peano.
 From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
-- 
GitLab