| Age | Commit message (Expand) | Author |
|---|
| 2015-12-07 | Fix some typos. | Guillaume Melquiond |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2015-09-03 | 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-07-22 | Extraction: fix primitive projection extraction. | Matthieu Sozeau |
| 2015-06-22 | Add efficient extraction of [nat], [Z], and [string] to Haskell | Nickolai Zeldovich |
| 2015-04-13 | Fixing bug #4186. | Pierre-Marie Pédrot |
| 2015-04-09 | 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-08 | 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-02 | 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-03-21 | 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-02-12 | Univs: fix bug #3978: carry around the universe context used to | Matthieu Sozeau |
| 2015-01-23 | Fix previous commit on extraction. | Maxime Dénès |
| 2015-01-23 | Extraction: fix #3629. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-11 | 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 |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-11-25 | Fix order of arguments in Extract Constant for Pos.compare_cont. | Maxime Dénès |
| 2014-10-28 | 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-27 | Fix some typos in comments. | Guillaume Melquiond |
| 2014-10-13 | library/opaqueTables: enable their use in interactive mode | Enrico Tassi |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-06-13 | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-06 | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau |
| 2014-05-06 | Fix a pervasive equality use. | Matthieu Sozeau |
| 2014-05-06 | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
