From 1019cb48c80260d7df27096826e8594ec242dc5a Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Thu, 7 May 2020 14:12:00 +0200
Subject: rename Bool.leb into Bool.le (same for ltb and compareb)

---
 theories/Sets/Uniset.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Sets')

diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 31e8cf463e..474b417e8e 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -44,18 +44,18 @@ Definition In (s:uniset) (a:A) : Prop := charac s a = true.
 Hint Unfold In : core.
 
 (** uniset inclusion *)
-Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a).
+Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a).
 Hint Unfold incl : core.
 
 (** uniset equality *)
 Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
 Hint Unfold seq : core.
 
-Lemma leb_refl : forall b:bool, leb b b.
+Lemma le_refl : forall b, Bool.le b b.
 Proof.
 destruct b; simpl; auto.
 Qed.
-Hint Resolve leb_refl : core.
+Hint Resolve le_refl : core.
 
 Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
 Proof.
-- 
cgit v1.2.3