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, 3 insertions, 3 deletions

diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index f8df97489..2bf3d8c35 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -138,7 +138,7 @@ Qed.
 
 Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].
 Proof.
-unfold Zlt; intros x y H;
+intros x y H.
 do 2 rewrite (same_genZ sor.(SORsetoid) ring_ops_wd sor.(SORrt));
 destruct x; destruct y; simpl in *; try discriminate.
 apply phi_pos1_pos.
@@ -146,8 +146,8 @@ now apply clt_pos_morph.
 apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
 apply (Rlt_trans sor) with 0. apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
 apply phi_pos1_pos.
-rewrite Pcompare_antisym in H; simpl in H. apply -> (Ropp_lt_mono sor).
-now apply clt_pos_morph.
+apply -> (Ropp_lt_mono sor); apply clt_pos_morph.
+red. now rewrite Pos.compare_antisym.
 Qed.
 
 Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y].