aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrfun.v
AgeCommit message (Expand)Author
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