Modularization of BinPos + fixes in Stdlib

 BinPos now contain a sub-module Pos, in which are placed functions
 like add (ex-Pplus), mul (ex-Pmult), ... and properties like
 add_comm, add_assoc, ...

 In addition to the name changes, the organisation is changed quite
 a lot, to try to take advantage more of the orders < and <= instead
 of speaking only of the comparison function.

 The main source of incompatibilities in scripts concerns this compare:
 Pos.compare is now a binary operation, expressed in terms of the
 ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
 this ternary version being called now Pos.compare_cont. As for everything
 else, compatibility notations (only parsing) are provided. But notations
 "_ ?= _" on positive will have to be edited, since they now point to
 Pos.compare.

 We also make the sub-module Pos to be directly an OrderedType,
 and include results about min and max.

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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index 750da2397..375ed0f90 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -8,7 +8,7 @@
 
 (** Definition of a square root function for N. *)
 
-Require Import BinPos BinNat Psqrt.
+Require Import BinPos BinNat.
 
 Local Open Scope N_scope.
 
@@ -16,7 +16,7 @@ Definition Nsqrtrem n :=
  match n with
   | N0 => (N0, N0)
   | Npos p =>
-    match Psqrtrem p with
+    match Pos.sqrtrem p with
      | (s, IsPos r) => (Npos s, Npos r)
      | (s, _) => (Npos s, N0)
     end
@@ -25,26 +25,26 @@ Definition Nsqrtrem n :=
 Definition Nsqrt n :=
  match n with
   | N0 => N0
-  | Npos p => Npos (Psqrt p)
+  | Npos p => Npos (Pos.sqrt p)
  end.
 
 Lemma Nsqrtrem_spec : forall n,
  let (s,r) := Nsqrtrem n in n = s*s + r /\ r <= 2*s.
 Proof.
  destruct n. now split.
- generalize (Psqrtrem_spec p). simpl.
+ generalize (Pos.sqrtrem_spec p). simpl.
  destruct 1; simpl; subst; now split.
 Qed.
 
 Lemma Nsqrt_spec : forall n,
  let s := Nsqrt n in s*s <= n < (Nsucc s)*(Nsucc s).
 Proof.
- destruct n. now split. apply (Psqrt_spec p).
+ destruct n. now split. apply (Pos.sqrt_spec p).
 Qed.
 
 Lemma Nsqrtrem_sqrt : forall n, fst (Nsqrtrem n) = Nsqrt n.
 Proof.
  destruct n. reflexivity.
- unfold Nsqrtrem, Nsqrt, Psqrt.
- destruct (Psqrtrem p) as (s,r). now destruct r.
+ unfold Nsqrtrem, Nsqrt, Pos.sqrt.
+ destruct (Pos.sqrtrem p) as (s,r). now destruct r.
 Qed.
\ No newline at end of file