aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/json.ml
AgeCommit message (Expand)Author
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