Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.le

Ack-by: Zimmi48
Reviewed-by: anton-trunov

5 files changed, 43 insertions, 38 deletions

diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst
index 7c10d261a7..42e5eb96eb 100644
--- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst
+++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst
@@ -1,5 +1,5 @@
 - **Added:**
-  Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``.
+  Order relations ``lt`` and ``compare`` added in ``Bool.Bool``.
   Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx``
   (`#12008 <https://github.com/coq/coq/pull/12008>`_,
   by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst
new file mode 100644
index 0000000000..6a4070a82e
--- /dev/null
+++ b/doc/changelog/10-standard-library/12162-bool-leb.rst
@@ -0,0 +1,4 @@
+- **Deprecated:**
+  ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported.
+  (`#12162 <https://github.com/coq/coq/pull/12162>`_,
+  by Olivier Laurent).
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 57cc8c4e90..d70978fabe 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -82,34 +82,39 @@ Qed.
 (** * Order on booleans *)
 (************************)
 
-Definition leb (b1 b2:bool) :=
+#[ local ] Definition le (b1 b2:bool) :=
   match b1 with
     | true => b2 = true
     | false => True
   end.
-Hint Unfold leb: bool.
+Hint Unfold le: bool.
 
-Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true.
+Lemma le_implb : forall b1 b2, le b1 b2 <-> implb b1 b2 = true.
 Proof.
   destr_bool; intuition.
 Qed.
 
-Definition ltb (b1 b2:bool) :=
+#[deprecated(since="8.12",note="Use Bool.le instead.")]
+Notation leb := le (only parsing).
+#[deprecated(since="8.12",note="Use Bool.le_implb instead.")]
+Notation leb_implb := le_implb (only parsing).
+
+#[ local ] Definition lt (b1 b2:bool) :=
   match b1 with
     | true => False
     | false => b2 = true
   end.
-Hint Unfold ltb: bool.
+Hint Unfold lt: bool.
 
-Definition compareb (b1 b2 : bool) :=
+#[ local ] Definition compare (b1 b2 : bool) :=
   match b1, b2 with
    | false, true => Lt
    | true, false => Gt
    | _, _ => Eq
   end.
 
-Lemma compareb_spec : forall b1 b2,
-  CompareSpec (b1 = b2) (ltb b1 b2) (ltb b2 b1) (compareb b1 b2).
+Lemma compare_spec : forall b1 b2,
+  CompareSpec (b1 = b2) (lt b1 b2) (lt b2 b1) (compare b1 b2).
 Proof. destr_bool; auto. Qed.
 
 
@@ -935,8 +940,8 @@ Defined.
 
 (** Notations *)
 Module BoolNotations.
-Infix "<=" := leb : bool_scope.
-Infix "<" := ltb : bool_scope.
-Infix "?=" := compareb (at level 70) : bool_scope.
+Infix "<=" := le : bool_scope.
+Infix "<" := lt : bool_scope.
+Infix "?=" := compare (at level 70) : bool_scope.
 Infix "=?" := eqb (at level 70) : bool_scope.
 End BoolNotations.
diff --git a/theories/Bool/BoolOrder.v b/theories/Bool/BoolOrder.v
index 61aab607a9..aaa7321bfc 100644
--- a/theories/Bool/BoolOrder.v
+++ b/theories/Bool/BoolOrder.v
@@ -14,69 +14,65 @@
 
 Require Export Bool.
 Require Import Orders.
-
-Local Notation le := Bool.leb.
-Local Notation lt := Bool.ltb.
-Local Notation compare := Bool.compareb.
-Local Notation compare_spec := Bool.compareb_spec.
+Import BoolNotations.
 
 (** * Order [le] *)
 
-Lemma le_refl : forall b, le b b.
+Lemma le_refl : forall b, b <= b.
 Proof. destr_bool. Qed.
 
 Lemma le_trans : forall b1 b2 b3,
-  le b1 b2 -> le b2 b3 -> le b1 b3.
+  b1 <= b2 -> b2 <= b3 -> b1 <= b3.
 Proof. destr_bool. Qed.
 
-Lemma le_true : forall b, le b true.
+Lemma le_true : forall b, b <= true.
 Proof. destr_bool. Qed.
 
-Lemma false_le : forall b, le false b.
+Lemma false_le : forall b, false <= b.
 Proof. intros; constructor. Qed.
 
-Instance le_compat : Proper (eq ==> eq ==> iff) le.
+Instance le_compat : Proper (eq ==> eq ==> iff) Bool.le.
 Proof. intuition. Qed.
 
 (** * Strict order [lt] *)
 
-Lemma lt_irrefl : forall b, ~ lt b b.
+Lemma lt_irrefl : forall b, ~ b < b.
 Proof. destr_bool; auto. Qed.
 
 Lemma lt_trans : forall b1 b2 b3,
-  lt b1 b2 -> lt b2 b3 -> lt b1 b3.
+  b1 < b2 -> b2 < b3 -> b1 < b3.
 Proof. destr_bool; auto. Qed.
 
-Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
+Instance lt_compat : Proper (eq ==> eq ==> iff) Bool.lt.
 Proof. intuition. Qed.
 
-Lemma lt_trichotomy : forall b1 b2, { lt b1 b2 } + { b1 = b2 } + { lt b2 b1 }.
+Lemma lt_trichotomy : forall b1 b2, { b1 < b2 } + { b1 = b2 } + { b2 < b1 }.
 Proof. destr_bool; auto. Qed.
 
-Lemma lt_total : forall b1 b2, lt b1 b2 \/ b1 = b2 \/ lt b2 b1.
+Lemma lt_total : forall b1 b2, b1 < b2 \/ b1 = b2 \/ b2 < b1.
 Proof. destr_bool; auto. Qed.
 
-Lemma lt_le_incl : forall b1 b2, lt b1 b2 -> le b1 b2.
+Lemma lt_le_incl : forall b1 b2, b1 < b2 -> b1 <= b2.
 Proof. destr_bool; auto. Qed.
 
-Lemma le_lteq_dec : forall b1 b2, le b1 b2 -> { lt b1 b2 } + { b1 = b2 }.
+Lemma le_lteq_dec : forall b1 b2, b1 <= b2 -> { b1 < b2 } + { b1 = b2 }.
 Proof. destr_bool; auto. Qed.
 
-Lemma le_lteq : forall b1 b2, le b1 b2 <-> lt b1 b2 \/ b1 = b2.
+Lemma le_lteq : forall b1 b2, b1 <= b2 <-> b1 < b2 \/ b1 = b2.
 Proof. destr_bool; intuition. Qed.
 
 
 (** * Order structures *)
 
 (* Class structure *)
-Instance le_preorder : PreOrder le.
+Instance le_preorder : PreOrder Bool.le.
 Proof.
 split.
 - intros b; apply le_refl.
 - intros b1 b2 b3; apply le_trans.
 Qed.
 
-Instance lt_strorder : StrictOrder lt.
+Instance lt_strorder : StrictOrder Bool.lt.
 Proof.
 split.
 - intros b; apply lt_irrefl.
@@ -88,13 +84,13 @@ Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder.
   Definition t := bool.
   Definition eq := @eq bool.
   Definition eq_equiv := @eq_equivalence bool.
-  Definition lt := lt.
+  Definition lt := Bool.lt.
   Definition lt_strorder := lt_strorder.
   Definition lt_compat := lt_compat.
-  Definition le := le.
+  Definition le := Bool.le.
   Definition le_lteq := le_lteq.
   Definition lt_total := lt_total.
-  Definition compare := compare.
+  Definition compare := Bool.compare.
   Definition compare_spec := compare_spec.
   Definition eq_dec := bool_dec.
   Definition eq_refl := @eq_Reflexive bool.
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.