index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
extraction
Commit message (
Expand
)
Author
Age
...
*
Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)
Pierre Letouzey
2015-12-14
*
Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)
Pierre Letouzey
2015-12-14
*
Extraction: cosmetically avoid generating spaces on empty lines
Pierre Letouzey
2015-12-14
*
Extraction: also get rid of explicit '\n' for haskell
Pierre Letouzey
2015-12-14
*
Extraction: fix a pretty-print issue
Pierre Letouzey
2015-12-14
*
Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")
Pierre Letouzey
2015-12-14
*
Extraction: nicer implementation of Implicits
Pierre Letouzey
2015-12-12
*
Extraction: check for remaining implicits after dead code removal (fix #4243)
Pierre Letouzey
2015-12-12
*
Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)
Pierre Letouzey
2015-12-12
*
Extraction: avoid generating some blanks at end-of-line
Pierre Letouzey
2015-12-12
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Improve directives for Haskell extraction of nat.
Maxime Dénès
2015-09-03
*
Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v
Nickolai Zeldovich
2015-09-03
*
Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v
Nickolai Zeldovich
2015-09-03
*
Extraction: fix primitive projection extraction.
Matthieu Sozeau
2015-07-22
*
Add efficient extraction of [nat], [Z], and [string] to Haskell
Nickolai Zeldovich
2015-06-22
*
Fixing bug #4186.
Pierre-Marie Pédrot
2015-04-13
*
JSON extraction: make explicit each group of mutually-recursive fixpoints
Nickolai Zeldovich
2015-04-09
*
JSON extraction: construct full names (dot-separated) in pp_global
Nickolai Zeldovich
2015-04-09
*
Add extraction to JSON.
Nickolai Zeldovich
2015-04-09
*
add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.v
Nickolai Zeldovich
2015-04-08
*
Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)
Nickolai Zeldovich
2015-04-08
*
Puts all the "import" statements first so as to accommodate the latest GHC.
Nickolai Zeldovich
2015-04-02
*
Fix some typos.
Guillaume Melquiond
2015-04-02
*
Define Any in Haskell extraction when Tunknown is used.
Nickolai Zeldovich
2015-04-02
*
Avoid segfault from code extracted to ghc. (Fix for bug #1257)
Guillaume Melquiond
2015-03-21
*
Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)
Guillaume Melquiond
2015-03-21
*
Do not revert parameter lists when extracting singleton types to Haskell. (Fi...
Guillaume Melquiond
2015-03-21
*
Univs: fix bug #3978: carry around the universe context used to
Matthieu Sozeau
2015-02-12
*
Fix previous commit on extraction.
Maxime Dénès
2015-01-23
*
Extraction: fix #3629.
Maxime Dénès
2015-01-23
*
Update headers.
Maxime Dénès
2015-01-12
*
Extraction: discard code unnecessary to fulfill a module signature
Pierre Letouzey
2015-01-11
*
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2015-01-11
*
Extraction: discard unnecessary code inside modules without signatures
Pierre Letouzey
2015-01-11
*
Extraction: no more ascii blob in type variables (fix #3227)
Pierre Letouzey
2015-01-11
*
Extraction : some more support functions for a future "Extraction Compute"
Pierre Letouzey
2015-01-11
*
Extraction: minor tweaks to ease ongoing experiments about Lambda
Pierre Letouzey
2015-01-11
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Fix order of arguments in Extract Constant for Pos.compare_cont.
Maxime Dénès
2014-11-25
*
Haskell extraction: use explicit -XMagicHash instead of -fglasgow-exts
Nickolai Zeldovich
2014-10-28
*
Haskell extraction: put unsafeCoerce type declaration later
Nickolai Zeldovich
2014-10-28
*
Fix some typos in comments.
Guillaume Melquiond
2014-10-27
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
[prev]
[next]