3 files changed, 10 insertions, 5 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 2da4452819..4aabda77ee 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -80,7 +80,7 @@ Proof.
  now apply testbit_even_succ.
 Qed.
 
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
 
 (** This concise equation could have been taken as specification
    for testbit in the interface, but it would have been hard to
@@ -102,10 +102,10 @@ Proof.
  left. destruct b; split; simpl; order'.
 Qed.
 
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
    power was initially taken as specification for testbit.
    We describe [a] as having a low part and a high part, with
-   the corresponding bit in the middle. This caracterisation
+   the corresponding bit in the middle. This characterisation
    is moderatly complex to implement, but also moderately
    usable... *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d7f25a6613..a70ecd19d8 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -13,7 +13,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
 (** * Euclidean Division for integers, Euclid convention
 
     We use here the "usual" formulation of the Euclid Theorem
-    [forall a b, b<>0 -> exists b q, a = b*q+r /\ 0 < r < |b| ]
+    [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b| ]
 
     The outcome of the modulo function is hence always positive.
     This corresponds to convention "E" in the following paper:
@@ -46,6 +46,7 @@ Module ZEuclidProp
 
  (** We put notations in a scope, to avoid warnings about
      redefinitions of notations *)
+ Declare Scope euclid.
  Infix "/" := D.div : euclid.
  Infix "mod" := D.modulo : euclid.
  Local Open Scope euclid.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 4b2d5c13b5..995d96b314 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -13,15 +13,18 @@
 Require Import NSub ZAxioms.
 Require Export Ring.
 
+Declare Scope pair_scope.
+Local Open Scope pair_scope.
+
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
-Local Open Scope pair_scope.
 
 Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig.
  Module Import NProp.
    Include NSubProp N.
  End NProp.
 
+Declare Scope NScope.
 Delimit Scope NScope with N.
 Bind Scope NScope with N.t.
 Infix "=="  := N.eq (at level 70) : NScope.
@@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2).
 
 End Z.
 
+Declare Scope ZScope.
 Delimit Scope ZScope with Z.
 Bind Scope ZScope with Z.t.
 Infix "=="  := Z.eq (at level 70) : ZScope.