coq - The formal proof system

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