| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-24 | Adding allsigs, the dependent version of allpairs | Cyril Cohen | |
| 2018-09-24 | Implementation 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-13 | Merge pull request #216 from CohenCyril/all_iff | Assia Mahboubi | |
| Small scale tool for proving circular implications, and using any pair of statements as an equivalence | |||
| 2018-09-13 | Small 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-12 | Merge pull request #228 from hivert/docfix | Cyril Cohen | |
| Fixes the doc of rat | |||
| 2018-09-11 | Fixes the doc of rat | Florent Hivert | |
| 2018-09-06 | Merge pull request #223 from math-comp/fix/compat-notation | Assia Mahboubi | |
| [warnings] -w "+compatibility-notation" clean | |||
| 2018-09-04 | [warnings] -w "+compatibility-notation" clean | Enrico Tassi | |
| 2018-08-06 | Merge pull request #208 from CohenCyril/companionmx | Laurent Théry | |
| Companion matrix of a polynomial | |||
| 2018-08-06 | changing companionmx to a more standard one | Cyril Cohen | |
| 2018-08-03 | update ChangeLog and doc | Cyril Cohen | |
| 2018-08-01 | Companion matrix of a polynomial | Cyril Cohen | |
| 2018-08-01 | Merge pull request #214 from CohenCyril/Makefile | Enrico | |
| simplified, cleaned and documented Makefile.common | |||
| 2018-08-01 | simplified, cleaned and documented Makefile.common | Cyril Cohen | |
| 2018-08-01 | Merge pull request #213 from CohenCyril/Makefile | Enrico | |
| Rework the whole Makefile architecture | |||
| 2018-07-31 | agressive fix for duplicated files! | Cyril Cohen | |
| 2018-07-31 | change coqdep | Cyril Cohen | |
| 2018-07-31 | some things should always be done | Cyril Cohen | |
| 2018-07-31 | removing dead code + reshuffling stuff | Cyril Cohen | |
| 2018-07-31 | Rework the whole Makefile architecture | Cyril 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-27 | Merge pull request #205 from anton-trunov/ssrnat-addnBAC-lemma | Cyril Cohen | |
| Add addnBAC lemma to ssrnat | |||
| 2018-07-24 | Add addnBAC, addnBCA, and addnABC lemmas to ssrnat | Anton Trunov | |
| Proofs by Cyril Cohen | |||
| 2018-07-19 | Merge pull request #202 from CohenCyril/improving-poly | Laurent Théry | |
| small generalizations and extensions in poly | |||
| 2018-07-19 | last_eq for exhaustivity | Cyril Cohen | |
| 2018-07-19 | poly_size_eq1 phrased with reflect + combinators | Cyril Cohen | |
| 2018-07-19 | Merge pull request #204 from pi8027/replace-coinductive-with-variant | Cyril Cohen | |
| Replace all the CoInductives with Variants | |||
| 2018-07-14 | updated proposition for big_prod_seq_eq1 | Cyril Cohen | |
| 2018-07-14 | Laurent's simplifications | Cyril Cohen | |
| 2018-07-12 | Replace all the CoInductives with Variants | Kazuhiko Sakaguchi | |
| 2018-07-04 | small generalizations in poly | Cyril Cohen | |
| 2018-07-02 | fix URL in README | Enrico | |
| Fix #200 | |||
| 2018-06-08 | Update INSTALL.md | Enrico | |
| 2018-06-08 | [INSTALL] document opam --root option | Enrico | |
| 2018-06-05 | Update CONTRIBUTING.md | Cyril Cohen | |
| 2018-06-05 | Update CONTRIBUTING.md | Cyril Cohen | |
| 2018-04-24 | replacing my local `git root` by a universal command | Cyril Cohen | |
| 2018-04-24 | fix opam packager script + dependencies | Cyril Cohen | |
| 2018-04-24 | Merge pull request #198 from math-comp/close-changelog-4-release | Cyril Cohen | |
| Close ChangeLog to release 1.7 | |||
| 2018-04-24 | fix typo | Enrico | |
| thanks Yves | |||
| 2018-04-24 | Update ChangeLog | Enrico | |
| 2018-04-24 | Merge pull request #197 from amahboubi/edit-changes | Enrico | |
| Improved ChangeLog | |||
| 2018-04-24 | Removed content about files not in the repo/release + minor stuff | Assia Mahboubi | |
| 2018-04-23 | Latest changes added to change log. | Assia Mahboubi | |
| 2018-04-23 | Improved ChangeLog | Assia Mahboubi | |
| One paragraph per version + spell check | |||
| 2018-04-20 | fix symlinks to README, INSTALL and LICENSE | Enrico Tassi | |
| 2018-04-20 | remove the attic/ directory | Enrico Tassi | |
| 2018-04-20 | remove ssr plugin for 8.4 and 8.5 | Enrico Tassi | |
| 2018-04-20 | update installation instructions | Enrico Tassi | |
| 2018-04-20 | move etc/ files to the root and remove obsolete ones | Enrico Tassi | |
| 2018-04-20 | generate the documentation for 1.7 | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |