aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/ssrfun.v
AgeCommit message (Expand)Author
2020-09-29new mem_imset lemmasChristian Doczkal
2019-11-22Added ssrfun theorem `inj_compr` (#432)Cyril Cohen
2019-10-25Instances for empty type. (#393)Arthur Azevedo de Amorim
2019-04-30Fix compatibility for #237Georges Gonthier
2019-04-29Generalise use of `{pred T}` from coq/coq#9995Georges Gonthier
2017-06-07For trunk, use merged ssr plugin.Maxime Dénès
2016-11-07update copyright bannerAssia Mahboubi
2015-07-28update copyright bannerEnrico Tassi
2015-07-18update to preserve backward compatibility with v8.4Cyril Cohen
2015-07-17Updating files + reorganizing everythingCyril Cohen
2015-03-09Initial commitEnrico Tassi