coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	New IR in VM: Clambda.	Maxime Dénès	2018-02-23
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Fix vm compiler to refuse to compile code making use of inductives with	Matthieu Sozeau	2015-03-25
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack	2007-12-18
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Changement des named_context	gregoire	2005-12-02
*	compatibility with POWERPC	gregoire	2004-11-22
*	bug module M:=N avec vm	barras	2004-11-17
*	COMMITED BYTECODE COMPILER	barras	2004-10-20