5 files changed, 101 insertions, 42 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 52ff725..1bb8aca 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -324,37 +324,36 @@ ci-bigenough-dev:
   variables:
     COQ_VERSION: "dev"
 
-# # The real-closed library
-# .ci-real-closed:
-#   extends: .ci
-#   variables:
-#     CONTRIB_URL: "https://github.com/math-comp/real-closed.git"
-#     CONTRIB_VERSION: master
-#   script:
-#     - opam pin add -n -k path coq-mathcomp-real-closed .
-#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed
-#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed
-# 
-# ci-real-closed-dev:
-#   extends: .ci-real-closed
-#   variables:
-#     COQ_VERSION: "dev"
-# 
-# # The analysis library
-# .ci-analysis:
-#   extends: .ci
-#   variables:
-#     CONTRIB_URL: "https://github.com/math-comp/analysis.git"
-#     CONTRIB_VERSION: master
-#   script:
-#     - opam pin add -n -k path coq-mathcomp-analysis .
-#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-analysis
-#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-analysis
-# 
-# ci-analysis-dev:
-#   extends: .ci-analysis
-#   variables:
-#     COQ_VERSION: "dev"
+# The real-closed library
+.ci-real-closed:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/real-closed.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-real-closed .
+    - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed
+
+ci-real-closed-8.10:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "8.10"
+
+ci-real-closed-8.11:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "8.11"
+
+ci-real-closed-8.12:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "8.12"
+
+ci-real-closed-dev:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "dev"
 
 # The finmap library
 .ci-finmap:
@@ -387,6 +386,63 @@ ci-finmap-dev:
   variables:
     COQ_VERSION: "dev"
 
+# The multinomials library
+.ci-multinomials:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/multinomials.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-multinomials .
+    - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-multinomials
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-multinomials
+
+ci-multinomials-8.10:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "8.10"
+
+ci-multinomials-8.11:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "8.11"
+
+ci-multinomials-8.12:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "8.12"
+
+ci-multinomials-dev:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "dev"
+
+# The analysis library
+.ci-analysis:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/analysis.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-analysis .
+    - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-analysis
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-analysis
+
+ci-analysis-8.11:
+  extends: .ci-analysis
+  variables:
+    COQ_VERSION: "8.11"
+
+ci-analysis-8.12:
+  extends: .ci-analysis
+  variables:
+    COQ_VERSION: "8.12"
+
+ci-analysis-dev:
+  extends: .ci-analysis
+  variables:
+    COQ_VERSION: "dev"
+
 # The FCSL-PCM library
 .ci-fcsl-pcm:
   extends: .ci
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6c52254..ad3cae2 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -24,6 +24,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Changed
 
+- In `ssralg.v` and `ssrint.v`, the nullary ring notations `-%R`, `+%R`, `*%R`,
+  `*:%R`, and `*~%R` are now declared in `fun_scope`.
+
 ### Renamed
 
 - in `path.v`,
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 8459c45..41147fb 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -3205,7 +3205,7 @@ Notation "@ 'divp_scalel'" :=
 Notation "@ 'divp_scaler'" :=
   (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope.
 Notation "@ 'divp_opp'" :=
-  (deprecate modp_opp divpN) (at level 10, only parsing) : fun_scope.
+  (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope.
 Notation "@ 'divp_add'" :=
   (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope.
 Notation modp_scalel := (@modp_scalel _) (only parsing).
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index d1f3072..de8b513 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -684,9 +684,9 @@ Definition opp V := Zmodule.opp (Zmodule.class V).
 Definition add V := Zmodule.add (Zmodule.class V).
 
 Local Notation "0" := (zero _) : ring_scope.
-Local Notation "-%R" := (@opp _) : ring_scope.
+Local Notation "-%R" := (@opp _) : fun_scope.
 Local Notation "- x" := (opp x) : ring_scope.
-Local Notation "+%R" := (@add _) : ring_scope.
+Local Notation "+%R" := (@add _) : fun_scope.
 Local Notation "x + y" := (add x y) : ring_scope.
 Local Notation "x - y" := (x + - y) : ring_scope.
 
@@ -980,7 +980,7 @@ Definition rreg R x := injective ((@mul R)^~ x).
 Local Notation "1" := (one _) : ring_scope.
 Local Notation "- 1" := (- (1)) : ring_scope.
 Local Notation "n %:R" := (1 *+ n) : ring_scope.
-Local Notation "*%R" := (@mul _).
+Local Notation "*%R" := (@mul _) : fun_scope.
 Local Notation "x * y" := (mul x y) : ring_scope.
 Local Notation "x ^+ n" := (exp x n) : ring_scope.
 
@@ -1606,7 +1606,7 @@ Import Lmodule.Exports.
 Definition scale (R : ringType) (V : lmodType R) : R -> V -> V :=
   Lmodule.scale (Lmodule.class V).
 
-Local Notation "*:%R" := (@scale _ _).
+Local Notation "*:%R" := (@scale _ _) : fun_scope.
 Local Notation "a *: v" := (scale a v) : ring_scope.
 
 Section LmoduleTheory.
@@ -1614,7 +1614,7 @@ Section LmoduleTheory.
 Variables (R : ringType) (V : lmodType R).
 Implicit Types (a b c : R) (u v : V).
 
-Local Notation "*:%R" := (@scale R V).
+Local Notation "*:%R" := (@scale R V) : fun_scope.
 
 Lemma scalerA a b v : a *: (b *: v) = a * b *: v.
 Proof. by case: V v => ? [] ? []. Qed.
@@ -6063,9 +6063,9 @@ Export Pred.Exports SubType.Exports.
 Notation QEdecFieldMixin := QEdecFieldMixin.
 
 Notation "0" := (zero _) : ring_scope.
-Notation "-%R" := (@opp _) : ring_scope.
+Notation "-%R" := (@opp _) : fun_scope.
 Notation "- x" := (opp x) : ring_scope.
-Notation "+%R" := (@add _).
+Notation "+%R" := (@add _) : fun_scope.
 Notation "x + y" := (add x y) : ring_scope.
 Notation "x - y" := (add x (- y)) : ring_scope.
 Notation "x *+ n" := (natmul x n) : ring_scope.
@@ -6079,14 +6079,14 @@ Notation "- 1" := (opp 1) : ring_scope.
 Notation "n %:R" := (natmul 1 n) : ring_scope.
 Notation "[ 'char' R ]" := (char (Phant R)) : ring_scope.
 Notation Frobenius_aut chRp := (Frobenius_aut chRp).
-Notation "*%R" := (@mul _).
+Notation "*%R" := (@mul _) : fun_scope.
 Notation "x * y" := (mul x y) : ring_scope.
 Notation "x ^+ n" := (exp x n) : ring_scope.
 Notation "x ^-1" := (inv x) : ring_scope.
 Notation "x ^- n" := (inv (x ^+ n)) : ring_scope.
 Notation "x / y" := (mul x y^-1) : ring_scope.
 
-Notation "*:%R" := (@scale _ _).
+Notation "*:%R" := (@scale _ _) : fun_scope.
 Notation "a *: m" := (scale a m) : ring_scope.
 Notation "k %:A" := (scale k 1) : ring_scope.
 Notation "\0" := (null_fun _) : ring_scope.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index 9ea0ce4..a51ec47 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -507,7 +507,7 @@ Definition intmul (R : zmodType) (x : R) (n : int) := nosimpl
     | Negz n => (x *- (n.+1))%R
   end.
 
-Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : ring_scope.
+Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : fun_scope.
 Notation "x *~ n" := (intmul x n)
   (at level 40, left associativity, format "x  *~  n") : ring_scope.
 Notation intr := ( *~%R 1).