coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	- Better error messages taking unif. constraints into account.	msozeau	2011-03-11
*	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
*	Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)	letouzey	2011-02-03
*	mli comments for doc	pboutill	2011-01-07
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Fixing Derive Inversion for new proof engine	herbelin	2010-05-26
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Take constraints into account in the "instantiate" tactic	herbelin	2009-10-30
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin	2009-08-11
*	Fixes to make Ynot compile with the trunk:	msozeau	2009-03-20
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	fixed problem with r11612	barras	2008-11-21
*	Partial fix for bug #1948: recompute order of dependencies between	msozeau	2008-09-25
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
*	Correction d'un bug de l'unification pattern qui oubliait d'expanser	herbelin	2008-05-20
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin	2008-03-10
*	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau	2008-02-08
*	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin	2007-09-26
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Correction d'un bug dans check_and_clear_in_constr + simplification de	notin	2007-01-31
*	Nouvelle implantation de clear_hyps	notin	2007-01-30
*	Correction du bug #1315:	notin	2007-01-22
*	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin	2006-09-15
*	Ajout unification pattern dans l'algorithme d'unification des	herbelin	2006-09-12
*	Prise en compte de l'instance des evars dans la détection des 'motifs'	herbelin	2006-08-29
*	Diverses modifications autour de l'unification modulo conversion:	herbelin	2006-08-28
*	Fixes for new unification, not used in default version as it really changes u...	msozeau	2006-04-10
*	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau	2006-04-10
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	Changement des named_context	gregoire	2005-12-02
*	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras	2005-06-07