aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
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
2014-11-25Fix order of arguments in Extract Constant for Pos.compare_cont.Maxime Dénès
2014-10-28Haskell extraction: use explicit -XMagicHash instead of -fglasgow-extsNickolai Zeldovich
2014-10-28Haskell extraction: put unsafeCoerce type declaration laterNickolai Zeldovich
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-13Deprecate options -dont, -lazy, -force-load-proofs.Guillaume Melquiond
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 20:56:54 +0000