aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-26correct and improve signature and documentation of FieldMixinGeorges Gonthier
Documentation of FieldUnitMixin and FieldMixin corrected to reflect actual arguments, with mulVf and inv0 made explicit arguments for FieldMixin (they were implicit due to the extended signature of Field.mixin_of). Type of FieldMixin changed to a convertible variant to facilitate construction of on-the-fly in-proof construction of fieldType instances, exposing an idomainType instance.
2018-11-24Merge pull request #249 from anton-trunov/prenex-implicitsCyril Cohen
Merge Arguments and Prenex Implicits
2018-11-21Merge Arguments and Prenex ImplicitsAnton Trunov
See the discussion here: https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
2018-11-19Improve documentation of phant_id usageGeorges Gonthier
Point out the use of id/idfun to control printing of notation. (as suggested by @anton-trunov - see #247)
2018-11-19Merge pull request #242 from anton-trunov/remove-canonical-for-mixinsGeorges Gonthier
Document and review the usage of canonical Equality mixins
2018-11-15Merge pull request #246 from anton-trunov/doc-commentsCyril Cohen
Add a section on documenting code
2018-11-15Tweak code related to canonical mixinsAnton Trunov
Remove some unused canonical mixins. Change simplification behavior of concrete comparison functions to allow for better simplification using unfolding and sebsequent folding back e.g. with `rewrite !eqE /= -!eqE`. A bit of cleanup for `Prenex Implicits` declarations. Document some explanations by G. Gonthier.
2018-11-15Add a section on documenting codeAnton Trunov
Based on the discussion here: https://github.com/math-comp/math-comp/pull/242
2018-11-13Documentation complements for combinatorial class factoriesGeorges Gonthier
Adding missing documentation for mixin and class constructors for Equality, Choice, Countable, and Finite. Renaming Equality mixin constructor comparableClass to the more consistent comparableMixin.
2018-11-13Ignore generated Makefile.coq.confGeorges Gonthier
2018-11-06Merge pull request #241 from ybertot/fix240Cyril Cohen
fix issue #240
2018-11-05fix issue #240Yves Bertot
2018-10-31Merge pull request #239 from CohenCyril/Make_bugEnrico
fixing local Makefiles
2018-10-31fixing local MakefileCyril Cohen
should fix #238
2018-10-30Merge pull request #236 from CohenCyril/allsigsCyril Cohen
Revert "Adding allsigs, the dependent version of allpairs"
2018-10-29Revert "Adding allsigs, the dependent version of allpairs"Cyril Cohen
This reverts commit 044634dcc2f645e3afbdad6cb8dcc66f3eb4a87e. See issue https://github.com/math-comp/odd-order/pull/5
2018-10-29Merge pull request #219 from CohenCyril/MakefileEnrico
fix some bugs in Makefile
2018-10-26Merge pull request #235 from CohenCyril/bool_irrelevance2Cyril Cohen
Statement of `bool_irrelevance` more consistent with its name.
2018-10-26fix some bugs in MakefileCyril Cohen
2018-10-26Statement of `bool_irrelevance` more consistent with its name.Cyril Cohen
2018-10-26Merge pull request #209 from CohenCyril/closed_fieldCyril Cohen
Moving countalg and closed_field around
2018-10-26moving countalg and closed_field aroundCyril Cohen
- countalg goes to the algebra package - finalg now get the expected inheritance from countalg - closed_field now contains the construction of algebraic closure for countable fields (previously in countalg) - proof of quantifier elimination for closed field rewritten in a monadic style
2018-10-26Merge pull request #218 from CohenCyril/taggedCyril Cohen
removing multiple definitions of [tT]ag*
2018-10-26removing multiple definitions of [tT]ag*Cyril Cohen
they are already defined in ssrfun ChangeLog updated
2018-10-25Merge pull request #234 from CohenCyril/ocaml4.05.0Enrico
bump ocaml version in travis
2018-10-25bump ocaml version in travisCyril Cohen
2018-10-25Merge pull request #232 from anton-trunov/masterEnrico
[opam]: add dev-repo links
2018-10-25Merge pull request #217 from CohenCyril/allsigsLaurent Théry
Adding `allsigs`, the dependent version of `allpairs`
2018-10-24Adding allsigs, the dependent version of allpairsCyril Cohen
2018-10-03[opam]: add dev-repo linksAnton Trunov
This commit fixes the following issue: ```shell $ opam pin add coq-mathcomp-ssreflect --dev [ERROR] "dev-repo" field missing in coq-mathcomp-ssreflect metadata, you'll need to specify the pinning location ``` This commit also changes http to https for the homepage links.
2018-09-24Implementation of all2 (#224)Pierre-Yves Strub
Added the definition of all2. This definition of all2 has the useful computational behaviour, and all2E unfolds an equivalent one.
2018-09-13Merge pull request #216 from CohenCyril/all_iffAssia Mahboubi
Small scale tool for proving circular implications, and using any pair of statements as an equivalence
2018-09-13Small scale tool for proving "the following are equivalent"Cyril Cohen
Tool to prove only P0 -> P1 -> ... -> Pn -> P0 but use any implication Pi -> Pj
2018-09-12Merge pull request #228 from hivert/docfixCyril Cohen
Fixes the doc of rat
2018-09-11Fixes the doc of ratFlorent Hivert
2018-09-06Merge pull request #223 from math-comp/fix/compat-notationAssia Mahboubi
[warnings] -w "+compatibility-notation" clean
2018-09-04[warnings] -w "+compatibility-notation" cleanEnrico Tassi
2018-08-06Merge pull request #208 from CohenCyril/companionmxLaurent Théry
Companion matrix of a polynomial
2018-08-06changing companionmx to a more standard oneCyril Cohen
2018-08-03update ChangeLog and docCyril Cohen
2018-08-01Companion matrix of a polynomialCyril Cohen
2018-08-01Merge pull request #214 from CohenCyril/MakefileEnrico
simplified, cleaned and documented Makefile.common
2018-08-01simplified, cleaned and documented Makefile.commonCyril Cohen
2018-08-01Merge pull request #213 from CohenCyril/MakefileEnrico
Rework the whole Makefile architecture
2018-07-31agressive fix for duplicated files!Cyril Cohen
2018-07-31change coqdepCyril Cohen
2018-07-31some things should always be doneCyril Cohen
2018-07-31removing dead code + reshuffling stuffCyril Cohen
2018-07-31Rework the whole Makefile architectureCyril Cohen
- Cleanup, refactoring and generalize the makefile architecture - Reuses @strub math-comp/analysis Makefile / Makefile.common organization - As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
2018-07-27Merge pull request #205 from anton-trunov/ssrnat-addnBAC-lemmaCyril Cohen
Add addnBAC lemma to ssrnat
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 11:02:09 +0000