aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/json.ml
AgeCommit message (Expand)Author
2019-02-04Primitive integersMaxime Dénès
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-06-07Put all plugins behind an "API".Matej Kosik
2016-10-17Fix bug #5023: JSON extraction doesn't generate "for xxx".Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-04-09JSON extraction: make explicit each group of mutually-recursive fixpointsNickolai Zeldovich
2015-04-09Add extraction to JSON.Nickolai Zeldovich