aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zsqrt_compat.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zsqrt_compat.v')
-rw-r--r--theories/ZArith/Zsqrt_compat.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index a6c832412..9e8d9372c 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -53,7 +53,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
| xI xH => c_sqrt 3 1 2 _ _
| xO (xO p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r') with
| left Hle =>
c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1)
@@ -63,7 +63,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
end
| xO (xI p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with
| left Hle =>
c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1)
@@ -74,7 +74,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
end
| xI (xO p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with
| left Hle =>
c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1)
@@ -85,7 +85,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
end
| xI (xI p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with
| left Hle =>
c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1)
@@ -114,7 +114,7 @@ Definition Zsqrt :
| Zpos p =>
fun h =>
match sqrtrempos p with
- | c_sqrt s r Heq Hint =>
+ | c_sqrt _ s r Heq Hint =>
existT
(fun s:Z =>
{r : Z |
@@ -150,7 +150,7 @@ Definition Zsqrt_plain (x:Z) : Z :=
match x with
| Zpos p =>
match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with
- | existT s _ => s
+ | existT _ s _ => s
end
| Zneg p => 0
| Z0 => 0