From e7df10a74264f52a17f54f87b8a89c9360a46926 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 16 Oct 2019 10:26:35 +0200
Subject: Redefine `normedDomainType` (now `normedZmodType`) (#392)

* Redefine `normedDomainType` (now `normedZmodType`)

- Redefine `normedDomainType` to drop ring and integral domain axioms.
- Add canonical instance of `normedZmodType` for `prod`.---
 mathcomp/field/algC.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index d41c6d8..aee2b85 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 normedDomainType := NormedDomainType type type numMixin.
+Canonical normedZmodType := NormedZmoduleType 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 normedDomainType := NormedDomainType type type numMixin.
+Canonical normedZmodType := NormedZmoduleType type type numMixin.
 Canonical numFieldType := [numFieldType of type].
 
 Lemma normK u : `|u| ^+ 2 = u * conj u.
@@ -541,7 +541,7 @@ Canonical comUnitRingType.
 Canonical idomainType.
 Canonical porderType.
 Canonical numDomainType.
-Canonical normedDomainType.
+Canonical normedZmodType.
 Canonical fieldType.
 Canonical numFieldType.
 Canonical decFieldType.
-- 
cgit v1.2.3