diff options
| author | Emilio Jesus Gallego Arias | 2016-09-20 12:35:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-09-20 12:35:11 +0200 |
| commit | 3bf6fbc4d339545b0eace0689adfec048f1c8530 (patch) | |
| tree | c1ff2fad749c8b5e813cdbc34683bcfb1bd0ff7e /mathcomp/field | |
| parent | b7796bb785b9d37e5b6648489d5c28e85df9d90d (diff) | |
[field] Remove unnecessary `Program Definition`
Simple `Definition` should work fine here.
This avoids the problem:
`Error: Library Coq.Program.Tactics has to be required first.`
in math-comp versions that depends on a minimal (or no) Coq stdlib.
Tested on 8.5/8.6
Diffstat (limited to 'mathcomp/field')
| -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. |