aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/ssrbool.v
AgeCommit message (Expand)Author
2020-11-24`in11(1)_sig` subsumes `in(2|3)_sig`Kazuhiko Sakaguchi
2020-11-24factoring out in_sigCyril Cohen
2020-11-01minimizing variablesCyril Cohen
2020-11-01generic interactions between in and onCyril Cohen
2020-08-11fix notation-incompatible-format warningsChristian Doczkal
2020-06-17contra lemmas involving propositionsChristian Doczkal
2020-06-08Documenting addition policy to coq.Cyril Cohen
2020-06-06bugfixCyril Cohen
2020-06-06Missing homo_mono lemmasCyril Cohen
2020-06-05Missing mono lemmas (#513)Cyril Cohen
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-12-20correct a typo in the documentationYves Bertot
2016-11-07update copyright bannerAssia Mahboubi
2016-04-08Fixing compilation after the merge of PR trunk-function_scope.Pierre-Marie Pédrot
2015-11-30Typos in comments.Assia Mahboubi
2015-11-20Typo.Assia Mahboubi
2015-11-20TyposAssia Mahboubi
2015-07-28update copyright bannerEnrico Tassi
2015-07-17Updating files + reorganizing everythingCyril Cohen
2015-03-09Initial commitEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:21:41 +0000