| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-24 | fix opam packager script + dependencies | Cyril Cohen | |
| 2018-04-20 | fix symlinks to README, INSTALL and LICENSE | Enrico Tassi | |
| 2018-04-20 | remove ssr plugin for 8.4 and 8.5 | Enrico Tassi | |
| 2018-04-17 | Removing undocumented compatibility module | Cyril 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-12 | ssrnat: 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-21 | Declare 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-20 | Merge pull request #185 from jashug/deprecate-arguments-scope | Enrico | |
| Change deprecated Arguments Scope to Arguments | |||
| 2018-03-06 | Merge pull request #178 from thery/master | Assia Mahboubi | |
| generalize the default value of nth in nth_iota | |||
| 2018-03-04 | Change deprecated Arguments Scope to Arguments | Jasper Hugunin | |
| 2018-03-03 | Merge pull request #179 from jashug/deprecate-implicit-arguments | Enrico | |
| Remove Implicit Arguments command in favor of Arguments | |||
| 2018-02-26 | Add ssrmatching.v transitional file | Erik 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-21 | Change Implicit Arguments to Arguments in ssreflect | Jasper Hugunin | |
| 2018-02-16 | generalize nth_iota | thery | |
| 2018-02-06 | fixing things that @ggonthier and @ybertot spotted and some I spotted | Cyril Cohen | |
| 2018-02-06 | running semi-automated linting on the whole library | Cyril Cohen | |
| 2018-02-05 | tide up proof of card_inj_ffuns | Enrico Tassi | |
| 2017-12-15 | Merge pull request #157 from ybertot/add-subset-orbit-theorems | Cyril Cohen | |
| Adds generalizations of theorems relying on injectivity | |||
| 2017-12-14 | Merge pull request #167 from hivert/PR2 | Cyril Cohen | |
| Resubmitted lemma reshape_index_leq for discussion | |||
| 2017-12-14 | Merge pull request #155 from erikmd/fix/gh-61 | Cyril Cohen | |
| Update v8.5 plugin to fix math-comp/math-comp#61 | |||
| 2017-12-12 | refactored proof and renamed to reshape_leq and removed spurious hypothesis | Cyril Cohen | |
| 2017-12-12 | bigop with allpairs | Florent Hivert | |
| 2017-12-12 | New lemma reshape_index_leq | Florent Hivert | |
| 2017-12-12 | shortening and refactoring | Cyril Cohen | |
| 2017-12-12 | Adds generalizations of theorems relying on injectivity | Yves 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-11 | Missing lemmas in seq | Florent Hivert | |
| 2017-11-21 | Merge pull request #115 from strub/uniqP | Cyril Cohen | |
| Reflection lemmas for `seq.uniq` | |||
| 2017-11-14 | Update v8.5 plugin to fix math-comp/math-comp#61 | Erik Martin-Dorel | |
| 2017-10-30 | Fix obsolete vernacular syntax for locality. | Maxime Dénès | |
| It was emitting a deprecation warning and will soon be removed from Coq. | |||
| 2017-10-23 | Remove compatibility with Coq.8.4 (and compatibility hacks that went with it) | Cyril Cohen | |
| 2017-10-23 | Merge pull request #145 from CohenCyril/new-packager | Cyril Cohen | |
| New packager | |||
| 2017-10-20 | Merge pull request #140 from RalfJung/make | Enrico | |
| fix building with make flags | |||
| 2017-10-19 | fixed homepage | Cyril Cohen | |
| 2017-10-19 | fix coq version | Cyril Cohen | |
| 2017-10-12 | fix Coq version detection on Windows, and in case there are errors | Ralf Jung | |
| 2017-10-10 | fix building with make flags | Ralf Jung | |
| Fixes #139 | |||
| 2017-09-13 | update the opam description for use in coq.8.7 | Yves Bertot | |
| 2017-09-07 | Merge pull request #106 from akr/remove-subfilter-doc | Cyril Cohen | |
| remove documentation for subfilter. | |||
| 2017-07-31 | Fix build of ssreflect/ only on 8.6 | Enrico Tassi | |
| 2017-07-13 | trunk -> master | Enrico | |
| 2017-06-14 | No .ml4 file in the standard Make | Enrico | |
| it is to the caller of coq_makefile to eventually add .ml4 files | |||
| 2017-06-14 | Fix compilation of ssreflect/ submodule | Matej Košík | |
| 2017-06-09 | fix compilation on 8.5 | Enrico Tassi | |
| 2017-06-09 | fix compilation on 8.6 | Enrico Tassi | |
| 2017-06-07 | For trunk, use merged ssr plugin. | Maxime Dénès | |
| 2017-06-06 | Fix plugin after Sigma removal. | Maxime Dénès | |
| 2017-06-06 | Merge pull request #127 from herbelin/trunk+interp_closed_glob_constr | Maxime Dénès | |
| Binding glob_constr to interp_glob_closure so as to factorize low-level code. | |||
| 2017-05-31 | Adapting to PR #590 (a more explicit algebraic type for evars of kind ↵ | Hugo Herbelin | |
| MatchingVar). | |||
| 2017-05-31 | Binding glob_constr to interp_glob_closure so as to factorize low-level code. | Hugo Herbelin | |
| 2017-05-25 | [coqlib] Update to explicitly build terms from references. | Emilio Jesus Gallego Arias | |
| See coq/coq#678 | |||
| 2017-05-25 | Merge pull request #125 from ejgallego/options+remove_non_sync | Maxime Dénès | |
| [options] Sync with upstream API changes. | |||
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |