coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	essai de typage des instantiations d\'evars	barras	2005-06-06
*	eradication de Evarutil.w_Define	barras	2005-06-05
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
*	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin	2004-12-08
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Suppression de Rawterm.loc, branchement sur Util.loc	herbelin	2004-07-16
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	Reparation d'une rupture (en presence de types implicites) de l'invariant que...	herbelin	2004-01-29
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin	2002-04-11
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	Introduction d'univers frais dans les types implicites engendrés par le pré...	herbelin	2001-11-08