Deletion of useless Zsqrt_def

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14245 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 18 insertions, 36 deletions

diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 3bdbca44a..d039fdcbf 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -574,15 +574,15 @@ Section ZModulo.
  generalize (Z_mod_lt [|x|] 2); omega.
  Qed.
 
- Definition sqrt x := Zsqrt [|x|].
+ Definition sqrt x := Z.sqrt [|x|].
  Lemma spec_sqrt : forall x,
        [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2.
  Proof.
  intros.
  unfold sqrt.
  repeat rewrite Zpower_2.
- replace [|Zsqrt [|x|]|] with (Zsqrt [|x|]).
- apply Zsqrt_spec; auto with zarith.
+ replace [|Z.sqrt [|x|]|] with (Z.sqrt [|x|]).
+ apply Z.sqrt_spec; auto with zarith.
  symmetry; apply Zmod_small.
  split. apply Z.sqrt_nonneg; auto.
  apply Zle_lt_trans with [|x|]; auto.
@@ -594,7 +594,7 @@ Section ZModulo.
   match z with
    | Z0 => (0, C0 0)
    | Zpos p =>
-      let (s,r) := Zsqrtrem (Zpos p) in
+      let (s,r) := Z.sqrtrem (Zpos p) in
       (s, if Z_lt_le_dec r wB then C0 r else C1 (r-wB))
    | Zneg _ => (0, C0 0)
   end.
@@ -610,8 +610,8 @@ Section ZModulo.
  remember ([|x|]*wB+[|y|]) as z.
  destruct z.
  auto with zarith.
- generalize (Zsqrtrem_spec (Zpos p)).
- destruct Zsqrtrem as (s,r); intros [U V]; auto with zarith.
+ generalize (Z.sqrtrem_spec (Zpos p)).
+ destruct Z.sqrtrem as (s,r); intros [U V]; auto with zarith.
  assert (s < wB).
   destruct (Z_lt_le_dec s wB); auto.
   assert (wB * wB <= Zpos p).
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 173a8f177..0bcf22e32 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -383,13 +383,13 @@ Module Make (N:NType) <: ZType.
   | Neg nx => Neg N.zero
   end.
 
- Theorem spec_sqrt: forall x, to_Z (sqrt x) = Zsqrt (to_Z x).
+ Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x).
  Proof.
   destruct x as [p|p]; simpl.
   apply N.spec_sqrt.
   rewrite N.spec_0.
   destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ].
-  rewrite Zsqrt_neg; auto with zarith.
+  rewrite Z.sqrt_neg; auto with zarith.
   now rewrite <- EQ.
  Qed.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 390b52ebe..dd83b65da 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -311,12 +311,12 @@ Qed.
 Lemma sqrt_spec : forall n, 0<=n ->
  (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)).
 Proof.
- intros n. zify. apply Zsqrt_spec.
+ intros n. zify. apply Z.sqrt_spec.
 Qed.
 
 Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0.
 Proof.
- intros n. zify. apply Zsqrt_neg.
+ intros n. zify. apply Z.sqrt_neg.
 Qed.
 
 (** Log2 *)
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index aabbf87f2..66b39aca9 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -771,7 +771,7 @@ Module Make (W0:CyclicType) <: NType.
   intros x. rewrite sqrt_fold. destr_t x as (n,x). exact (ZnZ.spec_sqrt x).
  Qed.
 
- Theorem spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
+ Theorem spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
  Proof.
   intros x.
   symmetry. apply Z.sqrt_unique.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 57277b489..9bed794f2 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -263,7 +263,7 @@ Qed.
 Lemma sqrt_spec : forall n, 0<=n ->
  (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)).
 Proof.
- intros n. zify. apply Zsqrt_spec.
+ intros n. zify. apply Z.sqrt_spec.
 Qed.
 
 Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 239d55cdc..5a927fe6b 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -13,7 +13,7 @@ Require Export ZArith_base.
 (** Extra definitions *)
 
 Require Export
- Zpow_def Zsqrt_def Zlog_def Zdigits_def.
+ Zpow_def Zlog_def Zdigits_def.
 
 (** Extra modules using [Omega] or [Ring]. *)
 
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index 1533eb925..4584c3f8f 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -11,12 +11,13 @@ Require Import Omega.
 Require Export ZArith_base.
 Open Local Scope Z_scope.
 
-(**    !! This file is deprecated !!
+(**  THIS FILE IS DEPRECATED
 
-    Please use rather Zsqrt_def.Zsqrt (or Zsqrtrem).
-    Unlike here, proofs there are fully separated from functions.
+    Instead of the various [Zsqrt] defined here, please use rather
+    [Z.sqrt] (or [Z.sqrtrem]). The latter are pure functions without
+    proof parts, and more results are available about them.
     Some equivalence proofs between the old and the new versions
-    can be found below. A Require Import ZArith provides by default
+    can be found below. Importing ZArith will provides by default
     the new versions.
 
 *)
diff --git a/theories/ZArith/Zsqrt_def.v b/theories/ZArith/Zsqrt_def.v
deleted file mode 100644
index 2012e8bcc..000000000
--- a/theories/ZArith/Zsqrt_def.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Definition of a square root function for Z. *)
-
-Require Import BinPos BinInt.
-
-Notation Zsqrtrem := Z.sqrtrem (only parsing).
-Notation Zsqrt := Z.sqrt (only parsing).
-Notation Zsqrtrem_spec := Z.sqrtrem_spec (only parsing).
-Notation Zsqrt_spec := Z.sqrt_spec (only parsing).
-Notation Zsqrt_neg := Z.sqrt_neg (only parsing).
-Notation Zsqrtrem_sqrt := Z.sqrtrem_sqrt (only parsing).
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 10c2d71b2..9605735dc 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -29,7 +29,6 @@ Zpower.vo
 Zpow_facts.vo
 Zsqrt_compat.vo
 Zwf.vo
-Zsqrt_def.vo
 Zlog_def.vo
 Zeuclid.vo
 Zdigits_def.vo
\ No newline at end of file