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/PArith/Pnat.v b/theories/PArith/Pnat.v
index 590217d5d..2984a7b5a 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -90,14 +90,14 @@ Qed.
 (** [nat_of_P] is a morphism for comparison *)
 
 Lemma Pcompare_nat_compare : forall p q,
- (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q).
+ (p ?= q) = nat_compare (nat_of_P p) (nat_of_P q).
 Proof.
  induction p as [ |p IH] using Pind; intros q.
  destruct (Psucc_pred q) as [Hq|Hq]; [now subst|].
  rewrite <- Hq, Plt_1_succ, Psucc_S, nat_of_P_xH, nat_compare_S.
  symmetry. apply nat_compare_lt, nat_of_P_pos.
  destruct (Psucc_pred q) as [Hq|Hq]; [subst|].
- rewrite ZC4, Plt_1_succ, Psucc_S. simpl.
+ rewrite Pos.compare_antisym, Plt_1_succ, Psucc_S. simpl.
  symmetry. apply nat_compare_gt, nat_of_P_pos.
  now rewrite <- Hq, 2 Psucc_S, Pcompare_succ_succ, IH.
 Qed.
@@ -250,21 +250,21 @@ Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Ppred_of_succ_nat_of_P
  (only parsing).
 
 Definition nat_of_P_minus_morphism p q :
- (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q
+ (p ?= q) = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q
  := fun H => Pminus_minus p q (ZC1 _ _ H).
 
 Definition nat_of_P_lt_Lt_compare_morphism p q :
- (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q
+ (p ?= q) = Lt -> nat_of_P p < nat_of_P q
  := proj1 (Plt_lt p q).
 
 Definition nat_of_P_gt_Gt_compare_morphism p q :
- (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q
+ (p ?= q) = Gt -> nat_of_P p > nat_of_P q
  := proj1 (Pgt_gt p q).
 
 Definition nat_of_P_lt_Lt_compare_complement_morphism p q :
- nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt
+ nat_of_P p < nat_of_P q -> (p ?= q) = Lt
  := proj2 (Plt_lt p q).
 
 Definition nat_of_P_gt_Gt_compare_complement_morphism p q :
- nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt
+ nat_of_P p > nat_of_P q -> (p ?= q) = Gt
  := proj2 (Pgt_gt p q).