6 files changed, 23 insertions, 13 deletions
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index 3ba9d1f5ed..7b6740e94b 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -23,6 +23,7 @@ Inductive positive : Set :=
   | xO : positive -> positive
   | xH : positive.
 
+Declare Scope positive_scope.
 Delimit Scope positive_scope with positive.
 Bind Scope positive_scope with positive.
 Arguments xO _%positive.
@@ -37,6 +38,7 @@ Inductive N : Set :=
   | N0 : N
   | Npos : positive -> N.
 
+Declare Scope N_scope.
 Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
 Arguments Npos _%positive.
@@ -53,6 +55,7 @@ Inductive Z : Set :=
   | Zpos : positive -> Z
   | Zneg : positive -> Z.
 
+Declare Scope Z_scope.
 Delimit Scope Z_scope with Z.
 Bind Scope Z_scope with Z.
 Arguments Zpos _%positive.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index ec480bb1eb..4a1f24b95e 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -21,7 +21,7 @@ Require Import Znumtheory.
 Require Import Zgcd_alt.
 Require Import Zpow_facts.
 Require Import CyclicAxioms.
-Require Import ROmega.
+Require Import Lia.
 
 Local Open Scope nat_scope.
 Local Open Scope int31_scope.
@@ -1237,7 +1237,7 @@ Section Int31_Specs.
   destruct (Z_lt_le_dec (X+Y) wB).
   contradict H1; auto using Zmod_small with zarith.
   rewrite <- (Z_mod_plus_full (X+Y) (-1) wB).
-  rewrite Zmod_small; romega.
+  rewrite Zmod_small; lia.
 
  generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq.
  destruct Z.compare; intros;
@@ -1261,7 +1261,7 @@ Section Int31_Specs.
   destruct (Z_lt_le_dec (X+Y+1) wB).
   contradict H1; auto using Zmod_small with zarith.
   rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB).
-  rewrite Zmod_small; romega.
+  rewrite Zmod_small; lia.
 
  generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq.
  destruct Z.compare; intros;
@@ -1299,8 +1299,8 @@ Section Int31_Specs.
   unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
   destruct (Z_lt_le_dec (X-Y) 0).
   rewrite <- (Z_mod_plus_full (X-Y) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
+  rewrite Zmod_small; lia.
+  contradict H1; apply Zmod_small; lia.
 
  generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq.
  destruct Z.compare; intros;
@@ -1318,8 +1318,8 @@ Section Int31_Specs.
   unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
   destruct (Z_lt_le_dec (X-Y-1) 0).
   rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
+  rewrite Zmod_small; lia.
+  contradict H1; apply Zmod_small; lia.
 
  generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq.
  destruct Z.compare; intros;
@@ -1356,7 +1356,7 @@ Section Int31_Specs.
  change [|1|] with 1; change [|0|] with 0.
  rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB).
  rewrite Zminus_mod_idemp_l.
- rewrite Zmod_small; generalize (phi_bounded x); romega.
+ rewrite Zmod_small; generalize (phi_bounded x); lia.
  Qed.
 
  Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 39af62c32f..77ab624ca5 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,8 +15,6 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
-Declare ML Module "int31_syntax_plugin".
-
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer
@@ -50,6 +48,8 @@ Inductive int31 : Type := I31 : digits31 int31.
 Register digits as int31 bits in "coq_int31" by True.
 Register int31 as int31 type in "coq_int31" by True.
 
+Declare Scope int31_scope.
+Declare ML Module "int31_syntax_plugin".
 Delimit Scope int31_scope with int31.
 Bind Scope int31_scope with int31.
 Local Open Scope int31_scope.
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.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 3d0c005fd1..acebfcf1d2 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -220,8 +220,10 @@ End NZDomainProp.
 Module NZOfNat (Import NZ:NZDomainSig').
 
 Definition ofnat (n : nat) : t := (S^n) 0.
-Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
+
+Declare Scope ofnat.
 Local Open Scope ofnat.
+Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
 
 Lemma ofnat_zero : [O] == 0.
 Proof.