| Age | Commit message (Expand) | Author |
|---|
| 2016-08-19 | Remove errorlabstrm in favor of user_err | Emilio Jesus Gallego Arias |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-06-29 | A new infrastructure for warnings. | Maxime Dénès |
| 2016-06-25 | [feedback] Add optional ?loc parameter to loggers. | Emilio Jesus Gallego Arias |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-12-09 | bug fixes to vm computation + test cases. | Gregory Malecha |
| 2015-10-28 | Refine Gregory Malecha's patch on VM and universe polymorphism. | Maxime Dénès |
| 2015-10-28 | Adds support for the virtual machine to perform reduction of universe polymor... | Gregory Malecha |
| 2015-07-29 | Fixing some English misspelling. | Hugo Herbelin |
| 2015-07-05 | Fix handling of primitive projections in VM. | Maxime Dénès |
| 2015-06-23 | Add a Set Dump Bytecode command for debugging purposes. | Maxime Dénès |
| 2015-03-30 | fix code and bound for SWITCH instruction. | Benjamin Gregoire |
| 2015-03-27 | use a more compact representation of non-constant constructors | Benjamin Gregoire |
| 2015-03-26 | allows the vm to deal with inductive type with 8388607 constant constructors ... | Benjamin Gregoire |
| 2015-03-26 | Fix bug 4157, | Benjamin Gregoire |
| 2015-03-25 | Fix vm compiler to refuse to compile code making use of inductives with | Matthieu Sozeau |
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond |
| 2015-01-17 | Univs: Fix alias computation for VMs, computation of normal form of | Matthieu Sozeau |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-11-10 | Fix #3282: VM confused by let bindings in fixpoints. | Maxime Dénès |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2013-03-12 | invalid_arg instead of raise (Invalid_argement ...) | letouzey |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2012-12-19 | Array.create is deprecated | pboutill |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-13 | More monomorphizations | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-09-14 | Partial revert of Yann commit in order to use CLib.List when opening | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-05-17 | Modops: the strengthening functions can work without any env argument | letouzey |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-07-30 | better fix to bug #2319: types are compiled in the env of the bodies | barras |
| 2010-07-29 | fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate... | barras |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-09 | Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972) | herbelin |
| 2010-05-09 | Added a few informations about file lineages (for the most part in kernel) | herbelin |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2007-12-18 | Nettoyage de code en vue de la release. Plus de Warning: Unused | aspiwack |
