aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrfwd.ml
AgeCommit message (Expand)Author
2018-07-19Remove declare_object for SsrHave NoTCResolution.Maxime Dénès
2018-06-22[ssr] set: merge universe constraints before type checking the termEnrico Tassi
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-14Deprecate Refiner [evar_map ref] exported functions.Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
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-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-06Merge the ssr plugin.Maxime Dénès