Merge branch 'v8.6'

2 files changed, 5 insertions, 4 deletions

diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 96885d2f7a..20022c00ec 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -18,7 +18,6 @@ Require Import BinInt.
 Require Import Setoid.
 Require Export Ncring.
 Require Export Ncring_polynom.
-Import List.
 
 Set Implicit Arguments.
 
@@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}.
   | Z0 => 0
   | Zneg p => -(gen_phiPOS p)
   end.
- Notation "[ x ]" := (gen_phiZ x).
+ Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Local Open Scope ZMORPHISM.
 
  Definition get_signZ z :=
   match z with
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 7fcd6c08a7..f7757a18da 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -238,7 +238,6 @@ Section ALMOST_RING.
  Variable req : R -> R -> Prop.
  Notation "0" := rO.  Notation "1" := rI.
  Infix "==" := req. Infix "+" := radd.  Infix "* " := rmul.
- Infix "-" := rsub. Notation "- x" := (ropp x).
 
  (** Leibniz equality leads to a setoid theory and is extensional*)
  Lemma Eqsth : Equivalence (@eq R).
@@ -263,7 +262,7 @@ Section ALMOST_RING.
         -x = x and x - y = x + y *)
  Definition SRopp (x:R) := x. Notation "- x" := (SRopp x).
 
- Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y).
+ Definition SRsub x y := x + -y. Infix "-" := SRsub.
 
  Lemma SRopp_ext : forall x y, x == y -> -x == -y.
  Proof. intros x y H; exact H. Qed.
@@ -320,6 +319,8 @@ Section ALMOST_RING.
  Qed.
 
  End  SEMI_RING.
+ Infix "-" := rsub.
+ Notation "- x" := (ropp x).
 
  Variable Reqe : ring_eq_ext radd rmul ropp req.
    Add Morphism radd : radd_ext2.  exact (Radd_ext Reqe). Qed.