coq - the Coq proof assistant

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