diff options
| author | Georges Gonthier | 2015-12-01 09:04:07 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:07:17 +0000 |
| commit | bd8cf1baa6758fef61ba8bd9917dc16bd6150613 (patch) | |
| tree | 534378977e611870c5f2e82e8cd93e1b8200956e | |
| parent | 903a5e41e93449fe257e289e75ecb5e948b092fe (diff) | |
Document limitation of fieldExtType cloning
Default cloning requires a manifest field class.
| -rw-r--r-- | mathcomp/field/fieldext.v | 10 |
1 files 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. |