aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrfun.v
AgeCommit message (Expand)Author
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2019-11-18Adding `inj_compr` lemma in ssrfun.Cyril Cohen
2019-10-22Add a notation for the empty type.Arthur Azevedo de Amorim
2019-10-13fix rev_right_loop docAntonio Nikishaev
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-30fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interfaceGeorges Gonthier
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-11-07[doc] nodes in ssr are monospaceEnrico Tassi
2018-11-07multi line comments don't have a titleEnrico Tassi
2018-11-07[doc] adapt comments in plugins/ssr/*.v to coqdoc styleEnrico Tassi
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-07-25Replace all the CoInductives with Variants in the SSR pluginKazuhiko Sakaguchi
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04ssr: fix typo in doc commentAnton Trunov
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-06-06Merge the ssr plugin.Maxime Dénès