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

2 files changed, 6 insertions, 4 deletions

diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 67d15b499..7d795cf50 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -24,8 +24,8 @@ Require Import BigNumPrelude.
 Require Import CyclicAxioms.
 Require Import ROmega.
 
-Open Scope nat_scope.
-Open Scope int31_scope.
+Local Open Scope nat_scope.
+Local Open Scope int31_scope.
 
 Section Basics.
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 1168e7fd6..23c2c36a2 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -40,7 +40,9 @@ Inductive digits : Type := D0 | D1.
 (** The type [int31] has a unique constructor [I31] that expects
    31 arguments of type [digits]. *)
 
-Inductive int31 : Type := I31 : nfun digits size int31.
+Definition digits31 t := Eval compute in nfun digits size t.
+
+Inductive int31 : Type := I31 : digits31 int31.
 
 (* spiwack: Registration of the type of integers, so that the matchs in
    the functions below perform dynamic decompilation (otherwise some segfault
@@ -50,7 +52,7 @@ Register int31 as int31 type in "coq_int31" by True.
 
 Delimit Scope int31_scope with int31.
 Bind Scope int31_scope with int31.
-Open Scope int31_scope.
+Local Open Scope int31_scope.
 
 (** * Constants *)