coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Unification: Added a heuristic to solve problems of the form	herbelin	2012-03-26
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Discarding let-ins from the instances of the evars in the	herbelin	2011-12-04
*	Adds a pair of function in Evar_util to gather dependent evars in an	aspiwack	2011-11-23
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Continuing r1492 (useless changes were inadvertantly committed)	herbelin	2011-10-25
*	New strategy to infer return predicate of match construct when	herbelin	2011-10-25
*	More robust and uniform treatment of aliases in evarutil.ml	herbelin	2011-10-10
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	Passed conv_algo to evar_define and move call to solve_refl to	herbelin	2011-10-10
*	- Fix restrict_hyps to not allow filtering on a variable required to typechec...	msozeau	2011-06-07
*	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