aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/kernel.mllib
Commit message (Expand)AuthorAge
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Unify pre_env and envGravatar Maxime Dénès2018-05-28
* Remove vm_conv hook and reorganize kernel filesGravatar Maxime Dénès2018-05-28
* Moving the VM global data to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
* New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
* Safer VM interfacesGravatar Maxime Dénès2018-01-26
* Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Gravatar Hugo Herbelin2017-08-12
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
* Move univops from kernel to libraryGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Replace Typeops by Fast_typeopsGravatar Gaetan Gilbert2016-12-12
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* Please never mention .mli-only file in *.mllib (or future *.mlpack)Gravatar Pierre Letouzey2016-06-02
* Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 05:00:14 +0000