coq - The formal proof system

Age	Commit message (Expand)	Author
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-04	Backtrack sur la mémoïsation de nf_evar.	aspiwack
2009-02-27	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack
2009-02-06	pushed evar reduction in kernel	barras
2009-01-17	DISCLAIMER	puech
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
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