More improvements of BigN, BigZ, BigQ:

 - ring/field: detection of constants for ring/field,
   detection of power, potential use of euclidean division.
 - for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive
 - mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify.
   By the way, BigN.zify could still be improved (no insertion of positivity
   hyps yet, unlike the original zify).
 - debug of BigQ.qify (autorewrite was looping on spec_0).
 - for BigQ, start of a generic functor of properties QProperties.
 - BigQ now implements OrderedType, TotalOrder, and contains facts
   about min and max.

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

2 files changed, 3 insertions, 1 deletions

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index a9945e848c..ffa91706f7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -49,6 +49,7 @@ Module Type ZType.
  Parameter mul : t -> t -> t.
  Parameter square : t -> t.
  Parameter power_pos : t -> positive -> t.
+ Parameter power : t -> N -> t.
  Parameter sqrt : t -> t.
  Parameter div_eucl : t -> t -> t * t.
  Parameter div : t -> t -> t.
@@ -72,6 +73,7 @@ Module Type ZType.
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
  Parameter spec_square: forall x, [square x] = [x] *  [x].
  Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+ Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
  Parameter spec_sqrt: forall x, 0 <= [x] ->
    [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
  Parameter spec_div_eucl: forall x y,
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 3d53707eb8..bcecb6a8a2 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -255,5 +255,5 @@ Qed.
 End ZTypeIsZAxioms.
 
 Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z
+ <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
  := Z <+ ZTypeIsZAxioms.