aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/kernel.mllib
Commit message (Expand)AuthorAge
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
* Uint31 support.Gravatar Maxime Dénès2014-04-09
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20