aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/ssreflect.v
AgeCommit message (Expand)Author
2021-01-16Drop support for Coq 8.10 and deprecate the `deprecate` notationKazuhiko Sakaguchi
2020-11-23fixing [dup] for Coq 8.12Cyril Cohen
2020-11-11Intro pattern extensions for dup, swap and applyCyril Cohen
2019-05-17refactor `seq` permutation theoryGeorges Gonthier
2019-05-06add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma namesGeorges 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
2016-09-07fix commentEnrico
2016-09-07abstract_context utility lemmaEnrico
2016-06-16Port build system to trunk (ssrmatching merged in Coq)Enrico Tassi
2016-04-08Fixing compilation after the merge of PR trunk-function_scope.Pierre-Marie Pédrot
2016-01-12Move bullet initialization to ssreflect.vRobbert Krebbers
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:03:00 +0000