coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-12-04	Factoring(continued).	Arnaud Spiwack
2013-12-04	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-03-14	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau
2012-03-01	New version of recdef :	jforest
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2009-12-16	adding an option functional_induction_rewrite_dependent to make functional in...	jforest
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey