renaming NormedZmoduleType and NormedZmoduleMixin (#416)

* renaming
NormedZmoduleType -> NormedZmodType
NormedZmoduleMixin -> NormedZmodMixin
that looks more homogeneous with regard to naming conventions used so far

* update .gitlab-ci.yml

* typo

4 files changed, 16 insertions, 16 deletions

diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 15cc4fc..14b5035 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -576,7 +576,7 @@ Canonical rat_porderType := POrderType ring_display rat ratLeMixin.
 Canonical rat_distrLatticeType := DistrLatticeType rat ratLeMixin.
 Canonical rat_orderType := OrderType rat le_rat_total.
 Canonical rat_numDomainType := NumDomainType rat ratLeMixin.
-Canonical rat_normedZmodType := NormedZmoduleType rat rat ratLeMixin.
+Canonical rat_normedZmodType := NormedZmodType rat rat ratLeMixin.
 Canonical rat_numFieldType := [numFieldType of rat].
 Canonical rat_realDomainType := [realDomainType of rat].
 Canonical rat_realFieldType := [realFieldType of rat].
@@ -811,7 +811,7 @@ Qed.
 
 Require setoid_ring.Field_theory setoid_ring.Field_tac.
 
-Lemma rat_field_theory : 
+Lemma rat_field_theory :
   Field_theory.field_theory 0%Q 1%Q addq mulq subq oppq divq invq eq.
 Proof.
 split => //; first exact rat_ring_theory.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index fabe541..feaa884 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -434,7 +434,7 @@ Canonical int_porderType := POrderType ring_display int intOrdered.Mixin.
 Canonical int_distrLatticeType := DistrLatticeType int intOrdered.Mixin.
 Canonical int_orderType := OrderType int intOrdered.lez_total.
 Canonical int_numDomainType := NumDomainType int intOrdered.Mixin.
-Canonical int_normedZmodType := NormedZmoduleType int int intOrdered.Mixin.
+Canonical int_normedZmodType := NormedZmodType int int intOrdered.Mixin.
 Canonical int_realDomainType := [realDomainType of int].
 
 Section intOrderedTheory.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 36adce0..d607291 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.                                       *)
-(*   NormedZmoduleType 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]                                            *)
@@ -64,7 +64,7 @@ From mathcomp Require Import ssralg poly.
 (*   * ArchiField (A Real Field with the archimedean axiom)                   *)
 (*   archiFieldType == interface for an archimedean field.                    *)
 (*   ArchiFieldType T r                                                       *)
-(*                  == packs the archimeadean axiom r into an archiFieldType. *)
+(*                  == packs the archimedean axiom r into an archiFieldType.  *)
 (*                     The carrier T must have a real field type structure.   *)
 (*   [archiFieldType of T for S]                                              *)
 (*                  == T-clone of the archiFieldType structure S.             *)
@@ -310,8 +310,8 @@ Canonical zmodType.
 Coercion numDomain_normedZmodType : NumDomain.type >-> type.
 Canonical numDomain_normedZmodType.
 Notation normedZmodType R := (type (Phant R)).
-Notation NormedZmoduleType R T m := (@pack _ (Phant R) T _ m).
-Notation NormedZmoduleMixin := Mixin.
+Notation NormedZmodType R T m := (@pack _ (Phant R) T _ m).
+Notation NormedZmodMixin := Mixin.
 Notation "[ 'normedZmodType' R 'of' T 'for' cT ]" :=
   (@clone _ (Phant R) T cT _ idfun)
   (at level 0, format "[ 'normedZmodType'  R  'of'  T  'for'  cT ]") :
@@ -548,7 +548,7 @@ Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
 Definition porderType := @Order.POrder.Pack ring_display cT xclass.
 Definition numDomainType := @NumDomain.Pack cT xclass.
 Definition fieldType := @GRing.Field.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
 Definition porder_fieldType := @GRing.Field.Pack porderType xclass.
 Definition normedZmod_fieldType :=
   @GRing.Field.Pack normedZmodType xclass.
@@ -648,7 +648,7 @@ Definition fieldType := @GRing.Field.Pack cT xclass.
 Definition numFieldType := @NumField.Pack cT xclass.
 Definition decFieldType := @GRing.DecidableField.Pack cT xclass.
 Definition closedFieldType := @GRing.ClosedField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
 Definition porder_decFieldType := @GRing.DecidableField.Pack porderType xclass.
 Definition normedZmod_decFieldType :=
   @GRing.DecidableField.Pack normedZmodType xclass.
@@ -764,7 +764,7 @@ Definition porderType := @Order.POrder.Pack ring_display cT xclass.
 Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass.
 Definition orderType := @Order.Total.Pack ring_display cT xclass.
 Definition numDomainType := @NumDomain.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
 Definition zmod_distrLatticeType :=
   @Order.DistrLattice.Pack ring_display zmodType xclass.
 Definition ring_distrLatticeType :=
@@ -897,7 +897,7 @@ Definition orderType := @Order.Total.Pack ring_display cT xclass.
 Definition realDomainType := @RealDomain.Pack cT xclass.
 Definition fieldType := @GRing.Field.Pack cT xclass.
 Definition numFieldType := @NumField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
 Definition field_distrLatticeType :=
   @Order.DistrLattice.Pack ring_display fieldType xclass.
 Definition field_orderType := @Order.Total.Pack ring_display fieldType xclass.
@@ -996,7 +996,7 @@ Definition realDomainType := @RealDomain.Pack cT xclass.
 Definition fieldType := @GRing.Field.Pack cT xclass.
 Definition numFieldType := @NumField.Pack cT xclass.
 Definition realFieldType := @RealField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
 
 End ClassDef.
 
@@ -1084,7 +1084,7 @@ Definition realDomainType := @RealDomain.Pack cT xclass.
 Definition fieldType := @GRing.Field.Pack cT xclass.
 Definition numFieldType := @NumField.Pack cT xclass.
 Definition realFieldType := @RealField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
 
 End ClassDef.
 
@@ -5064,7 +5064,7 @@ Definition normedZmodMixin :
   @normed_mixin_of R [zmodType of U * V] (Num.RealDomain.class R) :=
   @Num.NormedMixin _ _ _ norm normD norm_eq0 normrMn normrN.
 
-Canonical normedZmodType := NormedZmoduleType R (U * V) normedZmodMixin.
+Canonical normedZmodType := NormedZmodType R (U * V) normedZmodMixin.
 
 Lemma prod_normE (x : U * V) : `|x| = Num.max `|x.1| `|x.2|. Proof. by []. Qed.
 
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index aee2b85..0e3005d 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -232,7 +232,7 @@ Canonical closedFieldType := ClosedFieldType type closedFieldAxiom.
 Parameter numMixin : numMixin idomainType.
 Canonical porderType := POrderType ring_display type numMixin.
 Canonical numDomainType := NumDomainType type numMixin.
-Canonical normedZmodType := NormedZmoduleType type type numMixin.
+Canonical normedZmodType := NormedZmodType type type numMixin.
 Canonical numFieldType := [numFieldType of type].
 
 Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType.
@@ -432,7 +432,7 @@ Definition numMixin : numMixin closedFieldType :=
   sval (ComplexNumMixin conjK conj_nt).
 Canonical porderType := POrderType ring_display type numMixin.
 Canonical numDomainType := NumDomainType type numMixin.
-Canonical normedZmodType := NormedZmoduleType type type numMixin.
+Canonical normedZmodType := NormedZmodType type type numMixin.
 Canonical numFieldType := [numFieldType of type].
 
 Lemma normK u : `|u| ^+ 2 = u * conj u.