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, 6 insertions, 6 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 2b199858f..49e7d7256 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -20,12 +20,12 @@ Module NSig_NAxioms (N:NType) <: NAxiomsSig.
 Delimit Scope NumScope with Num.
 Bind Scope NumScope with N.t.
 Local Open Scope NumScope.
-Notation "[ x ]" := (N.to_Z x) : NumScope.
-Infix "=="  := N.eq (at level 70) : NumScope.
-Notation "0" := N.zero : NumScope.
-Infix "+" := N.add : NumScope.
-Infix "-" := N.sub : NumScope.
-Infix "*" := N.mul : NumScope.
+Local Notation "[ x ]" := (N.to_Z x) : NumScope.
+Local Infix "=="  := N.eq (at level 70) : NumScope.
+Local Notation "0" := N.zero : NumScope.
+Local Infix "+" := N.add : NumScope.
+Local Infix "-" := N.sub : NumScope.
+Local Infix "*" := N.mul : NumScope.
 
 Hint Rewrite
  N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub : num.