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, 4 insertions, 6 deletions

diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 482a96f43..375646bbd 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -83,9 +83,8 @@ Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m +
 
 Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
 Proof.
- intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
- destruct Pcompare; auto.
- intro H; rewrite H; auto.
+ intros; unfold Zmax, Pmax. simpl.
+ case Pos.compare_spec; auto; congruence.
 Qed.
 
 Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
@@ -97,9 +96,8 @@ Qed.
 
 Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
 Proof.
-  intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H.
-  rewrite (Pcompare_Eq_eq _ _ H).
-  unfold Pminus; rewrite Pminus_mask_diag; reflexivity.
+  intros; simpl. case Pos.compare_spec; intros H.
+  now rewrite H, Pos.sub_diag.
   rewrite Pminus_Lt; auto.
   symmetry. apply Zpos_max_1.
 Qed.