BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)

 - In fact, Bind Scope has no retrospective effect. Since we don't want
  it inside functor, we use it late, and hence we are forced to use manual
  "Arguments Scope" commands.
 - Added syntax for power in BigN / BigZ / BigQ.
 - Added syntax p#q in BigQ for representing fractions (constructor BigQ.Qq)
   as in QArith. Display of a rational numeral is hence either an integer
   (constructor BigQ.Qz) or something like 6756 # 8798.
 - Fix of function BigQ.Qred that was not simplifing (67#1) into 67.
 - More tests in test-suite/output/NumbersSyntax.v

A nice one not in the test-suite:

Time Eval vm_compute in BigQ.red ((2/3)^(-100000) * (2/3)^(100000)).
     = 1
     : bigQ
Finished transaction in 3. secs (3.284206u,0.004s)

:-)

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

1 files changed, 26 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 2e7604b0d..1ec7960ae 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -31,6 +31,31 @@ Delimit Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
+(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
+Arguments Scope BigZ.Pos [bigN_scope].
+Arguments Scope BigZ.Neg [bigN_scope].
+Arguments Scope BigZ.to_Z [bigZ_scope].
+Arguments Scope BigZ.succ [bigZ_scope].
+Arguments Scope BigZ.pred [bigZ_scope].
+Arguments Scope BigZ.opp [bigZ_scope].
+Arguments Scope BigZ.square [bigZ_scope].
+Arguments Scope BigZ.add [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.sub [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.mul [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.div [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.eq [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.lt [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.le [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.eq [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.compare [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.min [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.max [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.power_pos [bigZ_scope positive_scope].
+Arguments Scope BigZ.sqrt [bigZ_scope].
+Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Infix "+" := BigZ.add : bigZ_scope.
@@ -38,6 +63,7 @@ Infix "-" := BigZ.sub : bigZ_scope.
 Notation "- x" := (BigZ.opp x) : bigZ_scope.
 Infix "*" := BigZ.mul : bigZ_scope.
 Infix "/" := BigZ.div : bigZ_scope.
+Infix "^" := BigZ.power_pos : bigZ_scope.
 Infix "?=" := BigZ.compare : bigZ_scope.
 Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
 Infix "<" := BigZ.lt : bigZ_scope.