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

0 files changed, 0 insertions, 0 deletions