aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2016-04-09Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vNickolai Zeldovich
2016-01-20Update copyright headers.Maxime Dénès
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-04Extraction: msg_notice instead of msg_info.Pierre Courtieu
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-16Extraction: slightly better heuristic for Obj.magic simplificationsPierre Letouzey
2015-12-16Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsPierre Letouzey
2015-12-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
2015-12-15Extraction: fix a few little glitches with my last commit (replacing unused v...Pierre Letouzey
2015-12-15Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Pierre Letouzey
2015-12-14Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Pierre Letouzey
2015-12-14Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Pierre Letouzey
2015-12-14Extraction: cosmetically avoid generating spaces on empty linesPierre Letouzey
2015-12-14Extraction: also get rid of explicit '\n' for haskellPierre Letouzey
2015-12-14Extraction: fix a pretty-print issuePierre Letouzey
2015-12-14Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Pierre Letouzey
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-12-12Extraction: check for remaining implicits after dead code removal (fix #4243)Pierre Letouzey
2015-12-12Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Pierre Letouzey
2015-12-12Extraction: avoid generating some blanks at end-of-linePierre Letouzey
2015-12-07Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-09-03Improve directives for Haskell extraction of nat.Maxime Dénès
2015-09-03Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.vNickolai Zeldovich
2015-09-03Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.vNickolai Zeldovich
2015-07-22Extraction: fix primitive projection extraction.Matthieu Sozeau
2015-06-22Add efficient extraction of [nat], [Z], and [string] to HaskellNickolai Zeldovich
2015-04-13Fixing bug #4186.Pierre-Marie Pédrot
2015-04-09JSON extraction: make explicit each group of mutually-recursive fixpointsNickolai Zeldovich
2015-04-09JSON extraction: construct full names (dot-separated) in pp_globalNickolai Zeldovich
2015-04-09Add extraction to JSON.Nickolai Zeldovich
2015-04-08add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.vNickolai Zeldovich
2015-04-08Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)Nickolai Zeldovich
2015-04-02Puts all the "import" statements first so as to accommodate the latest GHC.Nickolai Zeldovich
2015-04-02Fix some typos.Guillaume Melquiond
2015-04-02Define Any in Haskell extraction when Tunknown is used.Nickolai Zeldovich
2015-03-21Avoid segfault from code extracted to ghc. (Fix for bug #1257)Guillaume Melquiond
2015-03-21Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Guillaume Melquiond
2015-03-21Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Guillaume Melquiond
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-01-23Fix previous commit on extraction.Maxime Dénès
2015-01-23Extraction: fix #3629.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-11Extraction: discard unnecessary code inside modules without signaturesPierre Letouzey
2015-01-11Extraction: no more ascii blob in type variables (fix #3227)Pierre Letouzey
2015-01-11Extraction : some more support functions for a future "Extraction Compute"Pierre Letouzey
2015-01-11Extraction: minor tweaks to ease ongoing experiments about LambdaPierre Letouzey
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 21:13:46 +0000