diff options
| author | Cyril Cohen | 2016-09-28 10:37:06 +0200 |
|---|---|---|
| committer | GitHub | 2016-09-28 10:37:06 +0200 |
| commit | fa7635aa606c2e8a24e772bebe46786b1acb2539 (patch) | |
| tree | efb7571cae13bcab138a0cf0bf4a35c08f2bb04f /mathcomp | |
| parent | b0e2b308330a8c1e15e818d0381d457e93213cc1 (diff) | |
| parent | 3bf6fbc4d339545b0eace0689adfec048f1c8530 (diff) | |
Merge pull request #69 from ejgallego/dont-depend-on-program
[field] Remove unnecessary use of `Program Definition` use
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/field/algC.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 6c53127..cbcbc3a 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -445,8 +445,8 @@ rewrite -(fmorph_root CtoL_rmorphism) -map_poly_comp; congr (root _ _): pu0. by apply/esym/eq_map_poly; apply: fmorph_eq_rat. Qed. -Program Definition conjMixin := - ImaginaryMixin (svalP (imaginary_exists closedFieldType)) +Definition conjMixin := + ImaginaryMixin (svalP (imaginary_exists closedFieldType)) (fun x => esym (normK x)). Canonical numClosedFieldType := NumClosedFieldType type conjMixin. |