| Age | Commit message (Expand) | Author |
|---|---|---|
| 2019-11-29 | Return of PR #226: adds relevant theorems when fcycle f (orbit f x) and the n... | Cyril Cohen |
| 2019-11-14 | fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403) | Anton Trunov |
| 2019-04-29 | Generalise use of `{pred T}` from coq/coq#9995 | Georges Gonthier |
| 2019-04-26 | Cleaning Require and Require Imports | Cyril Cohen |
| 2019-03-20 | [doc] Mention that fingraph's connect computes the reflexive transitive closure | Erik Martin-Dorel |
| 2018-12-11 | Fix some new warnings emitted by Coq 8.10: | Anton Trunov |
| 2018-11-21 | Merge Arguments and Prenex Implicits | Anton Trunov |
| 2018-02-21 | Change Implicit Arguments to Arguments in ssreflect | Jasper Hugunin |
| 2017-12-12 | shortening and refactoring | Cyril Cohen |
| 2017-12-12 | Adds generalizations of theorems relying on injectivity | Yves Bertot |
| 2016-11-07 | update copyright banner | Assia Mahboubi |
| 2015-11-05 | merge basic/ into ssreflect/ | Enrico Tassi |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |