coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-21	Generic support for open terms in tactics	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-10-30	Take constraints into account in the "instantiate" tactic	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-11	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin
2009-03-20	Fixes to make Ynot compile with the trunk:	msozeau
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2008-11-21	fixed problem with r11612	barras
2008-09-25	Partial fix for bug #1948: recompute order of dependencies between	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-18	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin
2008-06-18	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin
2008-05-20	Correction d'un bug de l'unification pattern qui oubliait d'expanser	herbelin
2008-05-05	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2008-03-10	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin
2008-02-08	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-01-31	Correction d'un bug dans check_and_clear_in_constr + simplification de	notin
2007-01-30	Nouvelle implantation de clear_hyps	notin
2007-01-22	Correction du bug #1315:	notin
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-12	Ajout unification pattern dans l'algorithme d'unification des	herbelin
2006-08-29	Prise en compte de l'instance des evars dans la détection des 'motifs'	herbelin
2006-08-28	Diverses modifications autour de l'unification modulo conversion:	herbelin
2006-04-10	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-07	- Documentation of the Program tactics.	msozeau
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2005-12-02	Changement des named_context	gregoire
2005-06-07	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras
2005-06-06	essai de typage des instantiations d\'evars	barras
2005-06-05	eradication de Evarutil.w_Define	barras
2005-03-08	Fix bug #931: leave dependent evars as such for refine	herbelin
2004-12-08	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-07-16	Suppression de Rawterm.loc, branchement sur Util.loc	herbelin
2004-06-30	updated printing of evar context (may loop ?)	corbinea
2004-01-29	Reparation d'une rupture (en presence de types implicites) de l'invariant que...	herbelin
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-04-11	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin
2002-04-10	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin