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