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

diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out
index 1a8f4eff13..ae0cba600c 100644
--- a/test-suite/output/NumbersSyntax.out
+++ b/test-suite/output/NumbersSyntax.out
@@ -24,6 +24,8 @@ I31
      : BigN.t_
      = 37151199385380486
      : BigN.t_
+     = 1267650600228229401496703205376
+     : bigN
 2
      : BigZ.t_
 -1000000000000000000
@@ -36,6 +38,8 @@ I31
      : BigZ.t_
      = 37151199385380486
      : BigZ.t_
+     = 1267650600228229401496703205376
+     : BigZ.t_
 2
      : BigQ.t_
 -1000000000000000000
@@ -48,9 +52,16 @@ I31
      : bigQ
      = 37151199385380486
      : bigQ
-BigQ.Qq 6562%bigZ 456%bigN
+6562 # 456
      : BigQ.t_
-     = BigQ.Qq 3281%bigZ 228%bigN
+     = 3281 # 228
+     : bigQ
+     = -1 # 10000
+     : bigQ
+     = 100
+     : bigQ
+     = 515377520732011331036461129765621272702107522001
+       # 1267650600228229401496703205376
      : bigQ
-     = BigQ.Qq 1%bigZ 10000%bigN
+     = 1
      : bigQ