Merge PR #12768: Granting wish #12762: warning on duplicated catch-all pattern-matching clause with unused named variable

Reviewed-by: jfehrle
Reviewed-by: vbgl
Ack-by: gares

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index adffa1ded4..382538875d 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -138,12 +138,12 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   Fixpoint compare x y :=
     match x, y with
       | x~1, y~1 => compare x y
-      | x~1, _ => Gt
+      | _~1, _ => Gt
       | x~0, y~0 => compare x y
-      | x~0, _ => Lt
-      | 1, y~1 => Lt
+      | _~0, _ => Lt
+      | 1, _~1 => Lt
       | 1, 1 => Eq
-      | 1, y~0 => Gt
+      | 1, _~0 => Gt
     end.
 
   Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).