aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/json.ml
Commit message (Expand)AuthorAge
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Fix bug #5023: JSON extraction doesn't generate "for xxx".Gravatar Pierre-Marie Pédrot2016-10-17
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* JSON extraction: make explicit each group of mutually-recursive fixpointsGravatar Nickolai Zeldovich2015-04-09
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09