3 files changed, 11 insertions, 7 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 278e1bcffa..c2fa69e535 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
     We just ignore them here.
 *)
 
-Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A).
- Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b.
+Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A).
+ Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b.
 End EuclidSpec.
 
 Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z.
-Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z.
 
 Module ZEuclidProp
  (Import A : ZAxiomsSig')
  (Import B : ZMulOrderProp A)
  (Import C : ZSgnAbsProp A B)
- (Import D : ZEuclid' A).
+ (Import D : ZEuclid A).
+
+ (** We put notations in a scope, to avoid warnings about
+     redefinitions of notations *)
+ Infix "/" := D.div : euclid.
+ Infix "mod" := D.modulo : euclid.
+ Local Open Scope euclid.
 
  Module Import Private_NZDiv := Nop <+ NZDivProp A D B.
 
@@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul.
 Qed.
 
 End ZEuclidProp.
-
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 63fb5800c1..fec6e06837 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType.
  Proof.
  apply Bool.eq_iff_eq_true.
  rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
  Qed.
 
  Definition min n m := match compare n m with Gt => m | _ => n end.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 98949736cb..1425041a10 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  apply eq_iff_eq_true.
  rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
  Qed.
 
  Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.