7 files changed, 35 insertions, 25 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 *)
 
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 6e8ca37ca..2e7604b0d 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -46,11 +46,11 @@ Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
 Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 
-Open Scope bigZ_scope.
+Local Open Scope bigZ_scope.
 
 (** Some additional results about [BigZ] *)
 
-Theorem spec_to_Z: forall n:bigZ,
+Theorem spec_to_Z: forall n : bigZ,
   BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
 Proof.
 intros n; case n; simpl; intros p;
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index e2be10ad9..d3f4776a6 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
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 4cc867898..ba457ffb8 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -51,11 +51,11 @@ Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
 Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 
-Open Scope bigN_scope.
+Local Open Scope bigN_scope.
 
 (** Example of reasoning about [BigN] *)
 
-Theorem succ_pred: forall q:bigN,
+Theorem succ_pred: forall q : bigN,
   0 < q -> BigN.succ (BigN.pred q) == q.
 Proof.
 intros; apply succ_pred.
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.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 38542c12b..eb0237f4a 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -10,7 +10,8 @@
 
 (*i $Id$ i*)
 
-Require Import Field Qfield BigN BigZ QSig QMake.
+Require Export BigZ.
+Require Import Field Qfield QSig QMake.
 
 (** We choose for BigQ an implemention with
     multiple representation of 0: 0, 1/0, 2/0 etc.
@@ -43,6 +44,13 @@ Notation bigQ := BigQ.t.
 Delimit Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with BigQ.t.
+Bind Scope bigQ_scope with BigQ.t_.
+
+(** BUG: the previous Bind Scope don't seem to work, and idem with BigN/BigZ.
+    For instance "Check (BigQ.opp 10)" fails when bigQ_scope is closed.
+    (whereas "Check (Int31.add31 10 10)" is ok). Something with modules ?
+    Adding an Arguments Scope helps, but this isn't a satisfactory solution.
+*)
 
 Infix "+" := BigQ.add : bigQ_scope.
 Infix "-" := BigQ.sub : bigQ_scope.
@@ -58,7 +66,7 @@ Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope.
 Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope.
 Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
 
-Open Scope bigQ_scope.
+Local Open Scope bigQ_scope.
 
 (** [BigQ] is a setoid *)