coq - The formal proof system

Age	Commit message (Expand)	Author
2018-05-28	Unify pre_env and env	Maxime Dénès
2018-05-28	Remove vm_conv hook and reorganize kernel files	Maxime Dénès
2018-03-26	Moving the VM global data to a ML reference.	Pierre-Marie Pédrot
2018-02-23	New IR in VM: Clambda.	Maxime Dénès
2018-01-26	Safer VM interfaces	Maxime Dénès
2017-08-12	Moving 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-16	Move univops from kernel to library	Amin Timany
2017-06-16	Squashed commit of the following:	Amin Timany
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2016-12-12	Replace Typeops by Fast_typeops	Gaetan Gilbert
2016-07-03	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey
2016-06-02	Please never mention .mli-only file in .mllib (or future .mlpack)	Pierre Letouzey
2015-10-06	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-09	Machine arithmetic operations for native compiler.	Maxime Dénès
2014-04-09	Had to split Nativelambda in two files because of Retroknowledge	Maxime Dénès
2014-04-09	Uint31 support.	Maxime Dénès
2014-02-26	Lazyconstr -> Opaqueproof	Enrico Tassi
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-10-23	Cleared a purely declarative .ml file and moved its interface to intf/	ppedrot
2011-10-25	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey