| Age | Commit message (Expand) | Author |
|---|
| 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-05-13 | Safer typing primitives. | Pierre-Marie Pédrot |
| 2015-05-11 | Rationalizing a bit the interface of Hints. | Pierre-Marie Pédrot |
| 2015-05-05 | Fix bug #4212, congruence forgetting about some universe constraints. | Matthieu Sozeau |
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond |
| 2015-04-23 | Using tclZEROMSG instead of tclZERO in several places. | Pierre-Marie Pédrot |
| 2015-04-22 | Declarative mode: remaining goals are "given up" when closing blocks. | Arnaud Spiwack |
| 2015-04-15 | Remove dirty debug printing from funind. | Maxime Dénès |
| 2015-04-14 | Function now supports puniveres | jforest |
| 2015-04-14 | better debug in recdef | jforest |
| 2015-04-14 | Opaque implementation of auto tactics. | Pierre-Marie Pédrot |
| 2015-04-13 | correction of a bug reported by Tristan Crolard | jforest |
| 2015-04-13 | Fixing bug #4186. | Pierre-Marie Pédrot |
| 2015-04-10 | Fix #3590 for good this time, by changing the API, change's argument now | Matthieu Sozeau |
| 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-04-01 | Accomodating #4166 (providing "Require Import OmegaTactic" as a | Hugo Herbelin |
| 2015-03-31 | Declarative mode: fix proof modes. | Arnaud Spiwack |
| 2015-03-31 | Declarative mode: fix vernac classification. | Arnaud Spiwack |
| 2015-03-31 | Declarative mode: plug the specialised printers back. | Arnaud Spiwack |
| 2015-03-25 | Correcting a bug introduced by universes polymorphism | jforest |
| 2015-03-25 | correcting a bug with aliased when using Functional Scheme | forest |
| 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-03-13 | Declarative mode: make it so that unfocussing can only be done for closed sub... | Arnaud Spiwack |
| 2015-03-13 | Declarative mode: remove dead code. | Arnaud Spiwack |
| 2015-03-13 | Declarative mode: remove a superfluous [set_proof_mode]. | Arnaud Spiwack |
| 2015-03-13 | Declarative mode: fix the focus behaviour. | Arnaud Spiwack |
| 2015-03-13 | rewiring Czar printers that were disabled | Pierre Corbineau |
| 2015-03-11 | Fix double print in decl_mode. | Enrico Tassi |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-03-03 | Fix bug #3732: firstorder was using detyping to build existential | Matthieu Sozeau |
| 2015-03-03 | Fix bug #3590, keeping evars that are not turned into named metas by | Matthieu Sozeau |
| 2015-02-27 | Removing the unused field ltacrecvars of tactic internalization. | Pierre-Marie Pédrot |
| 2015-02-24 | Calling coq references lazily in plugin cc so as to support static linking of... | Hugo Herbelin |
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond |
| 2015-02-14 | Fixing OCaml 3.12 compilation. | Pierre-Marie Pédrot |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi |
| 2015-02-12 | Univs: fix bug #3978: carry around the universe context used to | Matthieu Sozeau |
| 2015-02-12 | Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) | Hugo Herbelin |
| 2015-02-12 | Capital letter in plugins. | Hugo Herbelin |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
