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

2 files changed, 20 insertions, 16 deletions

diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 322f43850c..fd8ad6d771 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -36,14 +36,16 @@ Extract Inductive N => "Big.big_int"
 
 (** Efficient (but uncertified) versions for usual functions *)
 
-Extract Constant Pplus => "Big.add".
-Extract Constant Psucc => "Big.succ".
-Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)".
-Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)".
-Extract Constant Pmult => "Big.mult".
-Extract Constant Pmin => "Big.min".
-Extract Constant Pmax => "Big.max".
-Extract Constant Pcompare =>
+Extract Constant Pos.add => "Big.add".
+Extract Constant Pos.succ => "Big.succ".
+Extract Constant Pos.pred => "fun n -> Big.max Big.one (Big.pred n)".
+Extract Constant Pos.sub => "fun n m -> Big.max Big.one (Big.sub n m)".
+Extract Constant Pos.mul => "Big.mult".
+Extract Constant Pos.min => "Big.min".
+Extract Constant Pos.max => "Big.max".
+Extract Constant Pos.compare =>
+ "fun x y -> Big.compare_case Eq Lt Gt x y".
+Extract Constant Pos.compare_cont =>
  "fun x y c -> Big.compare_case c Lt Gt x y".
 
 Extract Constant Nplus => "Big.add".
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 9044b93843..0136957724 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -33,14 +33,16 @@ Extract Inductive N => int [ "0" "" ]
 
 (** Efficient (but uncertified) versions for usual functions *)
 
-Extract Constant Pplus => "(+)".
-Extract Constant Psucc => "succ".
-Extract Constant Ppred => "fun n -> max 1 (n-1)".
-Extract Constant Pminus => "fun n m -> max 1 (n-m)".
-Extract Constant Pmult => "( * )".
-Extract Constant Pmin => "min".
-Extract Constant Pmax => "max".
-Extract Constant Pcompare =>
+Extract Constant Pos.add => "(+)".
+Extract Constant Pos.succ => "succ".
+Extract Constant Pos.pred => "fun n -> max 1 (n-1)".
+Extract Constant Pos.sub => "fun n m -> max 1 (n-m)".
+Extract Constant Pos.mul => "( * )".
+Extract Constant Pos.min => "min".
+Extract Constant Pos.max => "max".
+Extract Constant Pos.compare =>
+ "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
+Extract Constant Pos.compare_cont =>
  "fun x y c -> if x=y then c else if x<y then Lt else Gt".