aboutsummaryrefslogtreecommitdiff
path: root/kernel/kernel.mllib
AgeCommit message (Expand)Author
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-09-25Move the Lib section data into the kernel.Pierre-Marie Pédrot
2019-09-25Move cumulativity inference to the kernel.Pierre-Marie Pédrot
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2019-01-21Move inductive typecheck to file independent from positivity check.Gaëtan Gilbert
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-09-17[VM] Move structured_constant to VmvaluesMaxime Dénès
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2018-02-23New IR in VM: Clambda.Maxime Dénès
2018-01-26Safer VM interfacesMaxime Dénès
2017-08-12Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Hugo Herbelin
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-25[api] Put modules in order in API.{mli,ml}Emilio Jesus Gallego Arias
2017-06-16Move univops from kernel to libraryAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-07Put all plugins behind an "API".Matej Kosik
2016-12-12Replace Typeops by Fast_typeopsGaetan Gilbert
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-06-02Please never mention .mli-only file in *.mllib (or future *.mlpack)Pierre Letouzey
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-09Machine arithmetic operations for native compiler.Maxime Dénès
2014-04-09Had to split Nativelambda in two files because of RetroknowledgeMaxime Dénès
2014-04-09Uint31 support.Maxime Dénès
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:27:59 +0000