aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrbwd.ml
AgeCommit message (Expand)Author
2020-12-27Refactor cpattern into a recordLasse Blaauwbroek
2020-12-27Make ssrtermkind algebraic instead of a charLasse Blaauwbroek
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-05-03Remove legacy SSR API.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR code.Pierre-Marie Pédrot
2020-05-03Further porting of ssrcode.Pierre-Marie Pédrot
2020-05-03Wrap ssr tactics into V82.tactic.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-11-16Remove SSR profilingJim Fehrle
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04ssr: ipats: V82.tactic ~nf_evars:false everywhereEnrico Tassi
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
2018-02-27Update headers following #6543.Théo Zimmermann
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-06Merge the ssr plugin.Maxime Dénès