coq - The formal proof system

Age	Commit message (Expand)	Author
2008-09-02	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-05-28	introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...	barras
2008-05-21	refined the conversion oracle	barras
2008-05-05	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin
2008-04-20	Add the ability to give a transparent_state for conversion, to	msozeau
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-04-13	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin
2006-09-01	Ajout is_sort: test si se réduit en une sorte	herbelin
2006-08-28	Ajout whd_eta + export append_stack_list + petit nettoyage (dont maj de	herbelin
2006-05-13	Code mort	herbelin
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2006-04-14	replacing whd_betaiotaevar_preserving_vm_cast	jforest
2006-03-28	Correction bug/typo dans splay_prod_assum et ajout decomp_sort	herbelin
2005-12-02	Changement des named_context	gregoire
2005-03-15	Backtrack sur la substitution combinée avec l'instanciation en réponse à l...	herbelin
2005-03-10	A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...	herbelin
2005-02-18	Ajout splay_lambda	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-06-29	Essai de suppression de eta dans simpl (cf bug #779)	herbelin
2004-05-14	test de conversion laissait echapper exception NotConvertible	barras
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-01-22	ajout de whd_state dans l'interface	barras
2002-04-08	export de la fonction Reductionops.find_conclusion pour l'extraction	letouzey
2002-02-11	substitution et pattern modulo let	barras
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-06	corrections mineures suite au commit de restructuration du noyau	barras
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras