coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Integrated obligations/eterm and program well-founded fixpoint building to to...	msozeau	2012-03-14
*	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Correct application of head reduction.	msozeau	2012-02-20
*	Avoid unnecessary normalizations w.r.t. evars in Program.	msozeau	2012-02-15
*	- Fix dependency computation in eterm to not consider filtered variables.	msozeau	2012-02-14
*	Fix inductive coercion code in Program (bug #2378)	msozeau	2011-10-18
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin	2010-10-31
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.	msozeau	2010-06-30
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	- Show Obligation Tactic	msozeau	2010-01-14
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fixes in Program:	msozeau	2009-04-07
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20