aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/fingraph.v
AgeCommit message (Expand)Author
2020-10-29Switch from long suffixes to short suffixesKazuhiko Sakaguchi
2020-09-27some lemmas for disjointChristian Doczkal
2020-06-26fix "Nothing to inject" warningsChristian Doczkal
2020-06-18Apply suggestions from code reviewChristian Doczkal
2020-06-18add fcard_gt?P lemmas found in fourcolorChristian Doczkal
2020-05-16A few more revisionsKazuhiko Sakaguchi
2020-05-13Revise proofs in ssreflect/*.vKazuhiko Sakaguchi
2020-04-08fix typos in documentation: textAntonio Nikishaev
2019-11-29Return of PR #226: adds relevant theorems when fcycle f (orbit f x) and the n...Cyril Cohen
2019-11-14fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403)Anton Trunov
2019-04-29Generalise use of `{pred T}` from coq/coq#9995Georges Gonthier
2019-04-26Cleaning Require and Require ImportsCyril Cohen
2019-03-20[doc] Mention that fingraph's connect computes the reflexive transitive closureErik Martin-Dorel
2018-12-11Fix some new warnings emitted by Coq 8.10:Anton Trunov
2018-11-21Merge Arguments and Prenex ImplicitsAnton Trunov
2018-02-21Change Implicit Arguments to Arguments in ssreflectJasper Hugunin
2017-12-12shortening and refactoringCyril Cohen
2017-12-12Adds generalizations of theorems relying on injectivityYves Bertot
2016-11-07update copyright bannerAssia Mahboubi
2015-11-05merge basic/ into ssreflect/Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:34:20 +0000