aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/field
AgeCommit message (Expand)Author
2020-11-25Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entriesKazuhiko Sakaguchi
2020-11-25Generalize `allrel` to take two lists as argumentsKazuhiko Sakaguchi
2020-11-20Tuning simplifications using Arguments simpl nomatchCyril Cohen
2020-11-19Removing duplicate clears and turning the warning into an errorCyril Cohen
2020-11-19add declare scopesReynald Affeldt
2020-10-30Use `exp` rather than `X` for exponents of polynomialsKazuhiko Sakaguchi
2020-10-29Switch from long suffixes to short suffixesKazuhiko Sakaguchi
2020-10-07Turn class_of records into primitive records and get rid of the xclass idiomKazuhiko Sakaguchi
2020-09-03Lemmas reindex_omap and bigD1_ordCyril Cohen
2020-08-12Make [fieldExtType F of L] work for abstract instancesKazuhiko Sakaguchi
2020-06-09fix coq 8.12 warningsCyril Cohen
2020-06-08turning let into local definitionCyril Cohen
2020-06-08silencing warnings in individual packagesCyril Cohen
2020-06-06ImprovementsCyril Cohen
2020-06-06General theory of min and max, and use in ssrnumCyril Cohen
2020-04-09Merge pull request #431 from ppedrot/rm-constr-hint-declsaffeldt-aist
2020-04-08fix typos in documentation: textAntonio Nikishaev
2020-04-08Remove hint declarations using non-global definitions.Pierre-Marie Pédrot
2020-01-15Non-distributive latticeKazuhiko Sakaguchi
2019-12-28Refactoring and linting especially polydivKazuhiko Sakaguchi
2019-12-11renaming NormedZmoduleType and NormedZmoduleMixin (#416)affeldt-aist
2019-12-11Rename: (l|L)attice -> (d|D)istrLatticeKazuhiko Sakaguchi
2019-12-11order.v: remove Order.Def, export Order.Syntax by default, and put missing sc...Kazuhiko Sakaguchi
2019-12-11Redefine `normedDomainType` (now `normedZmodType`) (#392)Kazuhiko Sakaguchi
2019-12-11Rename `totalLatticeMixin` to `totalPOrderMixin` and several refactorKazuhiko Sakaguchi
2019-12-11Add (meet|join)_(l|r), some renamings, and small cleanupsKazuhiko Sakaguchi
2019-12-11Make an appropriate use of the order library everywhere (#278, #280, #282, #2...Kazuhiko Sakaguchi
2019-11-27Explicit `bigop` enumeration handlingGeorges Gonthier
2019-11-22New generalised induction idiom (#434)Georges Gonthier
2019-11-14typo (#412)Laurent Théry
2019-11-06Merge pull request #408 from chdoc/existsPnCyril Cohen
2019-11-06Merge pull request #406 from hivert/algebrasCyril Cohen
2019-11-04Fixed inheritance of fieldExt / fieldOver / splitting fieldFlorent Hivert
2019-11-04add existsPn/forallPn lemmasChristian Doczkal
2019-11-03Interface for commutative and commutative-unitary algebrasFlorent Hivert
2019-10-30Change the order of arguments in `ltngtP`Kazuhiko Sakaguchi
2019-05-17refactor `seq` permutation theoryGeorges Gonthier
2019-05-06add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma namesGeorges Gonthier
2019-04-29Generalise use of `{pred T}` from coq/coq#9995Georges Gonthier
2019-04-26Cleaning Require and Require ImportsCyril Cohen
2019-04-08switching to opam 2.0 formatCyril Cohen
2018-12-20Move-and-rename opam files to the root folderErik Martin-Dorel
2018-12-13Adjust implicits of cancellation lemmasGeorges Gonthier
2018-12-11Fix some new warnings emitted by Coq 8.10:Anton Trunov
2018-12-04Remove `_ : Type` from packed classesAnton Trunov
2018-12-04Merge pull request #253 from anton-trunov/argumentsGeorges Gonthier
2018-12-04Document parameter names whenever possibleAnton Trunov
2018-11-26correct and improve signature and documentation of FieldMixinGeorges Gonthier
2018-11-21Merge Arguments and Prenex ImplicitsAnton Trunov
2018-10-31fixing local MakefileCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:55:10 +0000