| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2007-05-11 | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack |
| 2006-07-22 | - Ajout d'un cast vm dans la syntaxe : x <: t | bgregoir |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-08-19 | Sur le conseil de X.Leroy: x=[||] devient Array.length x=0 | letouzey |
| 2004-11-22 | compatibility with POWERPC | gregoire |
| 2004-11-17 | bug module M:=N avec vm | barras |
