From bd8cf1baa6758fef61ba8bd9917dc16bd6150613 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Tue, 1 Dec 2015 09:04:07 +0000 Subject: Document limitation of fieldExtType cloning Default cloning requires a manifest field class. --- mathcomp/field/fieldext.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 6214ef0..234ad47 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -14,7 +14,10 @@ Require Import poly polydiv mxpoly generic_quotient. (* it simply combines the fieldType and FalgType F *) (* interfaces. *) (* [fieldExtType F of L] == a fieldExt F structure for a type L that has both *) -(* fieldType and FalgType F canonical structures. *) +(* FalgType F and fieldType canonical instances. The *) +(* field class instance must be manifest with explicit *) +(* comRing, idomain, and field mixins. If L has an *) +(* abstract field class should use the 'for' variant. *) (* [fieldExtType F of L for K] == a fieldExtType F structure for a type L *) (* that has an FalgType F canonical structure, given *) (* a K : fieldType whose unitRingType projection *) @@ -250,10 +253,7 @@ Notation fieldExtType R := (type (Phant R)). Notation "[ 'fieldExtType' F 'of' L ]" := (@pack _ (Phant F) L _ _ id _ _ _ _ id) (at level 0, format "[ 'fieldExtType' F 'of' L ]") : form_scope. -(*Notation "[ 'fieldExtType' F 'of' L 'for' K ]" := - (@FieldExt.pack _ (Phant F) L _ _ id K _ _ _ idfun) - (at level 0, format "[ 'fieldExtType' F 'of' L 'for' K ]") : form_scope. -*) + Notation "[ 'fieldExtType' F 'of' L 'for' K ]" := (@pack_eta _ (Phant F) L K _ _ id _ id) (at level 0, format "[ 'fieldExtType' F 'of' L 'for' K ]") : form_scope. -- cgit v1.2.3