Merge PR #12801: Put cyclic numbers in sort Set instead of Type

Ack-by: Zimmi48
Reviewed-by: anton-trunov

4 files changed, 18 insertions, 5 deletions

diff --git a/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh b/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh
new file mode 100644
index 0000000000..6a9cf78687
--- /dev/null
+++ b/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "12801" ] || [ "$CI_BRANCH" = "CyclicSet" ]; then
+
+    bignums_CI_REF=CyclicSet
+    bignums_CI_GITURL=https://github.com/VincentSe/bignums
+
+    coqprime_CI_REF=CyclicSet
+    coqprime_CI_GITURL=https://github.com/VincentSe/coqprime
+fi
diff --git a/doc/changelog/10-standard-library/12801-cyclic-set.rst b/doc/changelog/10-standard-library/12801-cyclic-set.rst
new file mode 100644
index 0000000000..9a07d78144
--- /dev/null
+++ b/doc/changelog/10-standard-library/12801-cyclic-set.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Change the sort of cyclic numbers from Type to Set. For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color.
+  See for example commit 6f62bda in bignums.
+  (`#12801 <https://github.com/coq/coq/pull/12801>`_,
+  by Vincent Semeria).
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 6470cd6c81..e3e8f532b3 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -99,7 +99,7 @@ Module ZnZ.
     lxor        : t -> t -> t }.
  
  Section Specs.
- Context {t : Type}{ops : Ops t}.
+ Context {t : Set}{ops : Ops t}.
 
  Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99).
 
@@ -221,7 +221,7 @@ Module ZnZ.
 
  Section WW.
 
- Context {t : Type}{ops : Ops t}{specs : Specs ops}.
+ Context {t : Set}{ops : Ops t}{specs : Specs ops}.
 
  Let wB := base digits.
 
@@ -284,7 +284,7 @@ Module ZnZ.
 
  Section Of_Z.
 
- Context {t : Type}{ops : Ops t}{specs : Specs ops}.
+ Context {t : Set}{ops : Ops t}{specs : Specs ops}.
 
  Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99).
 
@@ -325,7 +325,7 @@ End ZnZ.
 (** A modular specification grouping the earlier records. *)
 
 Module Type CyclicType.
- Parameter t : Type.
+ Parameter t : Set.
  Declare Instance ops : ZnZ.Ops t.
  Declare Instance specs : ZnZ.Specs ops.
 End CyclicType.
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v
index 3232e3afe0..165f9893ca 100644
--- a/theories/Numbers/Cyclic/Abstract/DoubleType.v
+++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v
@@ -54,7 +54,7 @@ Arguments W0 {znz}.
     (if depth = n).
 *)
 
-Fixpoint word (w:Type) (n:nat) : Type :=
+Fixpoint word (w:Set) (n:nat) : Set :=
  match n with
  | O => w
  | S n => zn2z (word w n)