aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
AgeCommit message (Collapse)Author
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-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-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-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-26fix some bugs in MakefileCyril Cohen
2018-10-26Statement of `bool_irrelevance` more consistent with its name.Cyril Cohen
2018-10-26removing multiple definitions of [tT]ag*Cyril Cohen
they are already defined in ssrfun ChangeLog updated
2018-10-25Merge pull request #232 from anton-trunov/masterEnrico
[opam]: add dev-repo links
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-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-04[warnings] -w "+compatibility-notation" cleanEnrico Tassi
2018-08-01simplified, cleaned and documented Makefile.commonCyril Cohen
2018-07-31agressive fix for duplicated files!Cyril Cohen
2018-07-31change coqdepCyril 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-24Add addnBAC, addnBCA, and addnABC lemmas to ssrnatAnton Trunov
Proofs by Cyril Cohen
2018-07-19Merge pull request #202 from CohenCyril/improving-polyLaurent Théry
small generalizations and extensions in poly
2018-07-19last_eq for exhaustivityCyril Cohen
2018-07-19poly_size_eq1 phrased with reflect + combinatorsCyril Cohen
2018-07-12Replace all the CoInductives with VariantsKazuhiko Sakaguchi
2018-04-24fix opam packager script + dependenciesCyril Cohen
2018-04-20fix symlinks to README, INSTALL and LICENSEEnrico Tassi
2018-04-20remove ssr plugin for 8.4 and 8.5Enrico Tassi
2018-04-17Removing undocumented compatibility moduleCyril Cohen
I had put this for compatibility with mathcomp 1.6 when we were still using svn, but I am afraid it got under the radar. We should decide - if we revert the change of `ltngtP`, - if we document (and extend) the compatibility module - or if we just remove the module and keep the change to `ltngtP` I am personally in favour of the last
2018-04-12ssrnat: don't use `fix n` but rather `fix name n`Enrico Tassi
This was the proof does not depend on the lemma name.
2018-03-21Declare prenex implicits for `Some_inj`Anton Trunov
This backports the changes from Coq's [PR #6911](https://github.com/coq/coq/pull/6911) And also fixes a typo in doc comments
2018-03-20Merge pull request #185 from jashug/deprecate-arguments-scopeEnrico
Change deprecated Arguments Scope to Arguments
2018-03-06Merge pull request #178 from thery/masterAssia Mahboubi
generalize the default value of nth in nth_iota
2018-03-04Change deprecated Arguments Scope to ArgumentsJasper Hugunin
2018-03-03Merge pull request #179 from jashug/deprecate-implicit-argumentsEnrico
Remove Implicit Arguments command in favor of Arguments
2018-02-26Add ssrmatching.v transitional fileErik Martin-Dorel
The content of this file is similar to that of ssrfun.v and aims to increase compatibility with Coq 8.6+ for third-party libraries that depend on both math-comp and ssrmatching.v Close #63
2018-02-21Change Implicit Arguments to Arguments in ssreflectJasper Hugunin
2018-02-16generalize nth_iotathery
2018-02-06fixing things that @ggonthier and @ybertot spotted and some I spottedCyril Cohen
2018-02-06running semi-automated linting on the whole libraryCyril Cohen
2018-02-05tide up proof of card_inj_ffunsEnrico Tassi
2017-12-15Merge pull request #157 from ybertot/add-subset-orbit-theoremsCyril Cohen
Adds generalizations of theorems relying on injectivity
2017-12-14Merge pull request #167 from hivert/PR2Cyril Cohen
Resubmitted lemma reshape_index_leq for discussion
2017-12-14Merge pull request #155 from erikmd/fix/gh-61Cyril Cohen
Update v8.5 plugin to fix math-comp/math-comp#61
2017-12-12refactored proof and renamed to reshape_leq and removed spurious hypothesisCyril Cohen
2017-12-12bigop with allpairsFlorent Hivert
2017-12-12New lemma reshape_index_leqFlorent Hivert
2017-12-12shortening and refactoringCyril Cohen
2017-12-12Adds generalizations of theorems relying on injectivityYves Bertot
- f_finv - finv_f - fconnect_sym - iter_order - iter_finv - cycle_orbit - fpath_finv (* I need to sub-theorems for this case. *) All generalizations are named "..._in" the existing theorems are now instances of the generalizations.
2017-12-11Missing lemmas in seqFlorent Hivert
2017-11-21Merge pull request #115 from strub/uniqPCyril Cohen
Reflection lemmas for `seq.uniq`
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 23:38:02 +0000