From 2fb42ce6b9b74a2c5f66e9fa9cb16745cdb85687 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 18 Aug 2020 22:49:00 +0200
Subject: Adapting theories to unused pattern-matching variable warning.

---
 theories/Structures/OrdersEx.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Structures')

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).
-- 
cgit v1.2.3