Commit 964ea47b authored by Olivier Laurent's avatar Olivier Laurent

overlay for coq/coq#12162

parent 49b8abe5
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
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.
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment