coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
*	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
*	Index keys instead of simply global references.	Matthieu Sozeau	2014-09-27
*	First version of keyed subterm selection in unification.	Matthieu Sozeau	2014-09-27
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Moved the Loadpath part of Library to its own file, and documented	ppedrot	2013-03-26
*	correct some ends of .mllib files (avoid a broken tolink.ml)	letouzey	2012-08-24
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey	2012-05-29
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20