| Age | Commit message (Expand) | Author |
|---|
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot |
| 2014-12-17 | Fix (actually, properly implement :) hashconsing of projections, | Matthieu Sozeau |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-12-16 | Fix for #3154: use CUnix.sys_command to call native compiler. | Maxime Dénès |
| 2014-12-15 | Fix treatment of universe context in typecheck inductive (was added | Matthieu Sozeau |
| 2014-12-14 | Fix merging of name maps in union of universe contexts. | Matthieu Sozeau |
| 2014-12-10 | Revert commit that inverted the preference for FFlex/FProj problems in | Matthieu Sozeau |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau |
| 2014-11-23 | Fix #3824. de Bruijn error in normalization of fixpoints. | Maxime Dénès |
| 2014-11-21 | Fix bug #3804. | Matthieu Sozeau |
| 2014-11-20 | Exporting the function handling side-effects only applied to terms. | Pierre-Marie Pédrot |
| 2014-11-19 | Slightly improving error messages when mismatch with Proof using at Qed time. | Hugo Herbelin |
| 2014-11-19 | Option -type-in-type continued (deactivate test for inferred sort of | Hugo Herbelin |
| 2014-11-12 | Cleaner interfaces for linking locations of native compiler. | Maxime Dénès |
| 2014-11-10 | Fix #3282: VM confused by let bindings in fixpoints. | Maxime Dénès |
| 2014-11-10 | Better printing of dynlink errors in native compiler. | Maxime Dénès |
| 2014-10-27 | Fix some typos in comments. | Guillaume Melquiond |
| 2014-10-24 | Remove an ununsed pattern and commented code in the kernel. | Matthieu Sozeau |
| 2014-10-24 | Fix retroknowledge for int31 division. | Maxime Dénès |
| 2014-10-24 | No hash consing across calls to the native compiler. | Maxime Dénès |
| 2014-10-22 | Pushing Pierre's factorization of names in goal context printing from | Hugo Herbelin |
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin |
| 2014-10-14 | Revert "Move eta-expansion after delta reduction in kernel reduction. This ma... | Matthieu Sozeau |
| 2014-10-13 | selective join/export of the safe_environment | Enrico Tassi |
| 2014-10-13 | STM: simplify how the term part of a side effect is retrieved | Enrico Tassi |
| 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-10-10 | Fix segfault in native compiler on int31 division. | Maxime Dénès |
| 2014-10-02 | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau |
| 2014-10-02 | Move eta-expansion after delta reduction in kernel reduction. This makes | Matthieu Sozeau |
| 2014-09-30 | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-24 | Make the retroknowledge marshalable. | Arnaud Spiwack |
| 2014-09-18 | Clean a bit of univ.ml, add credits. | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-10 | Fix generation of inductive elimination principle for primitive records. | Matthieu Sozeau |
| 2014-09-06 | Fix checker to handle projections with eta and universe polymorphism correctly. | Matthieu Sozeau |
| 2014-09-05 | Fix checker treatment of inductives using subst_instances instead of subst_un... | Matthieu Sozeau |
| 2014-09-05 | Rename eta_expand_ind_stacks, fix the one from the checker and adapt | Matthieu Sozeau |
| 2014-09-05 | Fix primitive projections declarations for inductive records. | Matthieu Sozeau |
| 2014-09-04 | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-09-01 | Coqide prints succesive hyps of the same type on 1 line | Pierre Boutillier |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-29 | Add test-suite file. Compute the name for the record binder in the | Matthieu Sozeau |
| 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-18 | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger... | Matthieu Sozeau |
| 2014-08-14 | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau |
