The compatibility module in ssrnum should now be for version 1.10

3 files changed, 32 insertions, 11 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 34ae7d6..36f9bb1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -145,7 +145,7 @@ coq-dev:
     - make install
   except:
     - /^experiment\/order$/
-    - /^pr-(270|388|402|419)$/
+    - /^pr-(270|388|402|419|446)$/
 
 ci-fourcolor-8.7:
   extends: .ci-fourcolor
@@ -182,7 +182,7 @@ ci-fourcolor-dev:
     - make install
   only:
     - /^experiment\/order$/
-    - /^pr-(270|388|402|419)$/
+    - /^pr-(270|388|402|419|446)$/
 
 ci-fourcolor-8.7-270:
   extends: .ci-fourcolor-270
@@ -194,6 +194,16 @@ ci-fourcolor-8.8-270:
   variables:
     COQ_VERSION: "8.8"
 
+ci-fourcolor-8.9-270:
+  extends: .ci-fourcolor-270
+  variables:
+    COQ_VERSION: "8.9"
+
+ci-fourcolor-8.10-270:
+  extends: .ci-fourcolor-270
+  variables:
+    COQ_VERSION: "8.10"
+
 ci-fourcolor-dev-270:
   extends: .ci-fourcolor-270
   variables:
@@ -210,7 +220,7 @@ ci-fourcolor-dev-270:
     - make install
   except:
     - /^experiment\/order$/
-    - /^pr-(270|388|402|419)$/
+    - /^pr-(270|388|402|419|446)$/
 
 ci-odd-order-8.7:
   extends: .ci-odd-order
@@ -247,7 +257,7 @@ ci-odd-order-dev:
     - make install
   only:
     - /^experiment\/order$/
-    - /^pr-(270|388|402|419)$/
+    - /^pr-(270|388|402|419|446)$/
 
 ci-odd-order-8.7-270:
  extends: .ci-odd-order-270
@@ -259,6 +269,16 @@ ci-odd-order-8.8-270:
  variables:
    COQ_VERSION: "8.8"
 
+ci-odd-order-8.9-270:
+ extends: .ci-odd-order-270
+ variables:
+   COQ_VERSION: "8.9"
+
+ci-odd-order-8.10-270:
+ extends: .ci-odd-order-270
+ variables:
+   COQ_VERSION: "8.10"
+
 ci-odd-order-dev-270:
   extends: .ci-odd-order-270
   variables:
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b4cc0ec..1d890d5 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -86,10 +86,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
     `ler_norm_sum`, `ler_norm_sub`, `ler_dist_add`, `ler_sub_norm_add`,
     `ler_sub_dist`, `ler_dist_dist`, `ler_dist_norm_add`, `ler_nnorml`,
     `ltr_nnorml`, `lter_nnormr`.
-  + The compatibility layer for the version 1.9 is provided as the
-    `ssrnum.mc_1_9` module. One may compile proofs compatible with the version
-    1.9 in newer versions by using the `mc_1_9.Num` module instead of the `Num`
-    module. However, instances of the number structures may require changes.
+  + The compatibility layer for the version 1.10 is provided as the
+    `ssrnum.mc_1_10` module. One may compile proofs compatible with the version
+    1.10 in newer versions by using the `mc_1_10.Num` module instead of the
+    `Num` module. However, instances of the number structures may require
+    changes.
 
 ### Renamed
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 1f6c0a4..05ac8ed 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -26,7 +26,7 @@ From mathcomp Require Import ssralg poly.
 (*   normedZmodType R                                                         *)
 (*                  == interface for a normed Zmodule structure indexed by    *)
 (*                     numDomainType R.                                       *)
-(*   NormedZmodType R T m                                                  *)
+(*   NormedZmodType R T m                                                     *)
 (*                  == pack the normed Zmodule mixin into a normedZmodType.   *)
 (*                     The carrier T must have an integral domain structure.  *)
 (*   [normedZmodType R of T for S]                                            *)
@@ -5039,7 +5039,7 @@ Export Num.RealLeMixin.Exports Num.RealLtMixin.Exports.
 Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin.
 
 (* compatibility module *)
-Module mc_1_9.
+Module mc_1_10.
 Module Num.
 (* If you failed to process the next line in the PG or the CoqIDE, replace    *)
 (* all the "ssrnum.Num" with "Top.Num" in this module to process them, and    *)
@@ -5617,4 +5617,4 @@ Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F]
    format "[ 'arg'  'maxr_' ( i  >  i0 ) F ]") : form_scope.
 
 End Num.
-End mc_1_9.
+End mc_1_10.