coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	romega: shorter trace (no more term lengths)	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: lots of dead code + a few refactored proofs	Pierre Letouzey	2017-05-22
*	romega: if it bugs again, at least do it with a short and quick error	Pierre Letouzey	2017-05-22
*	romega: discard constructor D_mono (shorter trace + fix a bug)	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: discard useless cosntructor P_NOP	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: revised proofs (mostly bullets instead of ;[\|\|\|])	Pierre Letouzey	2017-05-22
*	Reduce warning noise when compiling the standard library.	Guillaume Melquiond	2016-08-09
*	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Clean up a comment in plugins/romega/ReflOmegaCore	Jason Gross	2014-08-25
*	Grammar: "allowing to" is not proper English	Jason Gross	2014-08-25
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey	2009-10-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20