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

4 files changed, 9 insertions, 9 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index c3c6c96997..02f408fd85 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -139,8 +139,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     | xH =>
         match m with
         | Leaf => Leaf
-        | Node Leaf o Leaf => Leaf
-        | Node l o r => Node l None r
+        | Node Leaf _ Leaf => Leaf
+        | Node l _ r => Node l None r
         end
     | xO ii =>
         match m with
diff --git a/theories/Strings/ByteVector.v b/theories/Strings/ByteVector.v
index ac0323442a..144ffd59e0 100644
--- a/theories/Strings/ByteVector.v
+++ b/theories/Strings/ByteVector.v
@@ -42,7 +42,7 @@ Fixpoint to_Bvector {n : nat} (v : ByteVector n) : Bvector (n * 8) :=
 Fixpoint of_Bvector {n : nat} : Bvector (n * 8) -> ByteVector n :=
   match n with
   | 0 => fun _ => []
-  | S n' =>
+  | S _ =>
     fun v =>
       let (b0, v1) := uncons v in
       let (b1, v2) := uncons v1 in
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).
diff --git a/theories/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v
index fb7fbcf80b..f7a848d7a5 100644
--- a/theories/micromega/RingMicromega.v
+++ b/theories/micromega/RingMicromega.v
@@ -1122,8 +1122,8 @@ Definition simpl_cone (e:Psatz) : Psatz :=
                     end
     | PsatzMulE t1 t2 =>
       match t1 , t2 with
-        | PsatzZ      , x        => PsatzZ
-        |    x     , PsatzZ      => PsatzZ
+        | PsatzZ      , _        => PsatzZ
+        |    _     , PsatzZ      => PsatzZ
         | PsatzC c ,  PsatzC c' => PsatzC (ctimes c c')
         | PsatzC p1 , PsatzMulE (PsatzC p2)  x => PsatzMulE (PsatzC (ctimes p1 p2)) x
         | PsatzC p1 , PsatzMulE x (PsatzC p2)  => PsatzMulE (PsatzC (ctimes p1 p2)) x