coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2009-10-21	This big commit addresses two problems:	soubiran
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-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-07-06	change in the order of unification constraints solving (for canonical structu...	amahboub
2009-06-02	Backtrack on experimental unification with sort variables: it requires	msozeau
2009-05-28	Properly catch sort constraint inconsistency exception in	msozeau
2009-05-27	Populate the sort constraints set correctly during unification. Add a	msozeau
2009-05-23	A try at using sort variables during unification. Instead of refreshing	msozeau
2009-05-09	fix a bug in canonical structures (bug found and fixed by Cyril)	barras
2009-03-20	Fixes to make Ynot compile with the trunk:	msozeau
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-09	memoized is_ground_env	barras
2009-02-06	pushed evar reduction in kernel	barras
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2008-11-21	fixed problem with r11612	barras
2008-11-21	fixed exponential behavior of evar unif (ground case)	barras
2008-11-07	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau
2008-08-05	Correction de bugs:	herbelin
2008-08-05	Suite 11187 et 11298 : ne retarder le dépliage d'une projection	herbelin
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-06-29	Correction d'un bug dans l'analyse des contraintes non résolues	herbelin
2008-06-29	Préférence donnée aux constantes qui ne sont pas des projections	herbelin
2008-06-21	Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)	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-14	Résolution des problèmes ambigus d'inférence du type de retour des	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-02-19	added products and sorts as possible heads for canonical structures	corbinea
2008-02-14	Added default canonical structures (see example in test-suite)	corbinea
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-10-01	Amendement à la révision 10124 : déplacement de apprec_nohdbeta entre	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-06	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
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-29	Il faut (au moins) normaliser les evars avant de tenter	herbelin
2006-08-28	Diverses modifications autour de l'unification modulo conversion:	herbelin
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-03-02	Correctif pour bug #1089 (cannot define an isevar twice)	herbelin
2005-12-17	Orthographe de 'instantiate'	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
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