coq - The formal proof system

Age	Commit message (Expand)	Author
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
2005-05-20	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin
2005-02-18	Standardisation of function names about global references (especially, renami...	herbelin
2004-11-26	Correction bug #879	herbelin
2004-11-19	Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-09-15	hiding the meta_map in 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-06-25	correspondance des records et noms de champs de records entre un module et sa...	letouzey
2003-01-31	Unification plus efficace vis à vis du LetIn	herbelin
2003-01-23	reparation des contribs: lors de l'unification, reduire les beta redexes	barras
2003-01-22	modified the unification algorithm to try first order unification before	barras
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-06-07	L'ordre supérieur avait quelque peu été oublié dans l'unification...	herbelin
2002-04-11	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin