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

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

2 files changed, 5 insertions, 5 deletions

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)