Repair interpretation of numeral for BigQ, add a printer (close #2160)

 on the way:
 - Added a testsuite output file
 - Try to avoid nasty unfolding (fix nfun ...) in type of I31.
   Idealy we would need a "Eval compute in" for the type of a inductive
   constructor
 - Stop opening Scopes for BigQ, BigN, BigZ by default
   The user should do some Open Scope.

TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope
(and so on for other operations), even with some Bind Scope around.

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

1 files changed, 9 insertions, 9 deletions

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index e2be10ad95..d3f4776a6c 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -19,15 +19,15 @@ Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
 Delimit Scope NumScope with Num.
 Bind Scope NumScope with Z.t.
 Local Open Scope NumScope.
-Notation "[ x ]" := (Z.to_Z x) : NumScope.
-Infix "=="  := Z.eq (at level 70) : NumScope.
-Notation "0" := Z.zero : NumScope.
-Infix "+" := Z.add : NumScope.
-Infix "-" := Z.sub : NumScope.
-Infix "*" := Z.mul : NumScope.
-Notation "- x" := (Z.opp x) : NumScope.
-Infix "<=" := Z.le : NumScope.
-Infix "<" := Z.lt : NumScope.
+Local Notation "[ x ]" := (Z.to_Z x) : NumScope.
+Local Infix "=="  := Z.eq (at level 70) : NumScope.
+Local Notation "0" := Z.zero : NumScope.
+Local Infix "+" := Z.add : NumScope.
+Local Infix "-" := Z.sub : NumScope.
+Local Infix "*" := Z.mul : NumScope.
+Local Notation "- x" := (Z.opp x) : NumScope.
+Local Infix "<=" := Z.le : NumScope.
+Local Infix "<" := Z.lt : NumScope.
 
 Hint Rewrite
  Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ