aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
Commit message (Expand)AuthorAge
* mergeGravatar Matej Kosik2016-01-11
|\
| * CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\ \
| * | Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\| |
| * | Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
* | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\| |
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
| |/ |/|
| * Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
|/
* Extraction: slightly better heuristic for Obj.magic simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: more cautious use of intermediate result caching (fix #3923)Gravatar Pierre Letouzey2015-12-15
* Extraction: fix a few little glitches with my last commit (replacing unused v...Gravatar Pierre Letouzey2015-12-15
* Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Gravatar Pierre Letouzey2015-12-14
* Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Gravatar Pierre Letouzey2015-12-14
* Extraction: cosmetically avoid generating spaces on empty linesGravatar Pierre Letouzey2015-12-14
* Extraction: also get rid of explicit '\n' for haskellGravatar Pierre Letouzey2015-12-14
* Extraction: fix a pretty-print issueGravatar Pierre Letouzey2015-12-14
* Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Gravatar Pierre Letouzey2015-12-14
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Extraction: check for remaining implicits after dead code removal (fix #4243)Gravatar Pierre Letouzey2015-12-12
* Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Gravatar Pierre Letouzey2015-12-12
* Extraction: avoid generating some blanks at end-of-lineGravatar Pierre Letouzey2015-12-12
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Improve directives for Haskell extraction of nat.Gravatar Maxime Dénès2015-09-03
* Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.vGravatar Nickolai Zeldovich2015-09-03
* Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.vGravatar Nickolai Zeldovich2015-09-03
* Extraction: fix primitive projection extraction.Gravatar Matthieu Sozeau2015-07-22
* Add efficient extraction of [nat], [Z], and [string] to HaskellGravatar Nickolai Zeldovich2015-06-22
* Fixing bug #4186.Gravatar Pierre-Marie Pédrot2015-04-13
* JSON extraction: make explicit each group of mutually-recursive fixpointsGravatar Nickolai Zeldovich2015-04-09
* JSON extraction: construct full names (dot-separated) in pp_globalGravatar Nickolai Zeldovich2015-04-09
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
* add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.vGravatar Nickolai Zeldovich2015-04-08
* Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)Gravatar Nickolai Zeldovich2015-04-08
* Puts all the "import" statements first so as to accommodate the latest GHC.Gravatar Nickolai Zeldovich2015-04-02
* Fix some typos.Gravatar Guillaume Melquiond2015-04-02
* Define Any in Haskell extraction when Tunknown is used.Gravatar Nickolai Zeldovich2015-04-02
* Avoid segfault from code extracted to ghc. (Fix for bug #1257)Gravatar Guillaume Melquiond2015-03-21
* Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Gravatar Guillaume Melquiond2015-03-21
* Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Gravatar Guillaume Melquiond2015-03-21
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Fix previous commit on extraction.Gravatar Maxime Dénès2015-01-23
* Extraction: fix #3629.Gravatar Maxime Dénès2015-01-23
* Update headers.Gravatar Maxime Dénès2015-01-12
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Extraction: discard unnecessary code inside modules without signaturesGravatar Pierre Letouzey2015-01-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 13:27:24 +0000