diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-18 15:21:02 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-18 15:21:02 +0000 |
| commit | 5a932e8c77207188c73629da8ab80f4c401c4e76 (patch) | |
| tree | 8d010eb327dd2084661ab623bfb7a917a96f651a /theories/ZArith | |
| parent | f761bb2ac13629b4d6de8855f8afa4ea95d7facc (diff) | |
Unset Asymmetric Patterns
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zsqrt_compat.v | 12 |
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 |