aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/json.ml
Commit message (Expand)AuthorAge
* 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