aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.ml
Commit message (Expand)AuthorAge
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Array.create is deprecatedGravatar pboutill2012-12-19
* Modulification of identifierGravatar ppedrot2012-12-14
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* better fix to bug #2319: types are compiled in the env of the bodiesGravatar barras2010-07-30
* fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...Gravatar barras2010-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)Gravatar herbelin2010-05-09
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* compatibility with POWERPCGravatar gregoire2004-11-22
* bug module M:=N avec vmGravatar barras2004-11-17
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20