diff options
| author | Hugo Herbelin | 2020-08-18 22:49:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-05 16:19:12 +0200 |
| commit | 2fb42ce6b9b74a2c5f66e9fa9cb16745cdb85687 (patch) | |
| tree | 88d12d5f428c1dc89cb8cb272e3531a2d7a531de /theories | |
| parent | 571834b2b43e4281ef4940ee5894d8191588bb6c (diff) | |
Adapting theories to unused pattern-matching variable warning.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 4 | ||||
| -rw-r--r-- | theories/Strings/ByteVector.v | 2 | ||||
| -rw-r--r-- | theories/Structures/OrdersEx.v | 8 | ||||
| -rw-r--r-- | theories/micromega/RingMicromega.v | 4 |
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 |