coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-04-10	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin
2002-02-18	bug #134: on appelait solve_simple_eqn avec une evar qui etait resolue	barras
2001-11-05	GROS COMMIT:	barras
2001-10-29	Amérioration message d'erreur en cas d'échec du filtrage de premier ordre	herbelin
2001-10-16	Nettoyage Recordobj et conséquences	herbelin
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-07-06	la conversion ne doit être testé dans evar_conv qu'en absence de evar	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-15	Modification pour passage p-automates	mohring