| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
| * | Grammar: "allowing to" is not proper English | Jason Gross | 2014-08-25 |
| * | A tentative uniform naming policy in module Inductiveops. |  Hugo Herbelin | 2014-08-01 |
| * | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond | 2014-06-13 |
| * | Reuse universe level substitutions for template polymorphism, fixing performance |  Matthieu Sozeau | 2014-05-09 |
| * | 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 | 2014-05-06 |
| * | Using HMaps in global references. |  Pierre-Marie Pédrot | 2014-03-08 |
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
| * | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot | 2014-03-03 |
| * | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
| * | New compilation mode -vi2vo | Enrico Tassi | 2014-02-26 |
| * | More monomorphic List.mem + List.assoc + ... |  letouzey | 2013-10-24 |
| * | Turn many List.assoc into List.assoc_f | letouzey | 2013-10-24 |
| * | cList.index is now cList.index_f, same for index0 | letouzey | 2013-10-23 |
Nickolai Zeldovich
Guillaume Melquiond
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Enrico Tassi
Arnaud Spiwack
Jason Gross
Hugo Herbelin
Matthieu Sozeau
Pierre-Marie Pédrot
letouzey