coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-06-07	- Added two new introduction patterns with the following temptative syntaxes:	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-03-22	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin
2006-01-28	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2004-07-16	Nouvelle en-tête	herbelin
2003-05-19	Restructuration des procédures de filtrage	herbelin
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2002-06-05	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin
2002-06-05	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin
2002-05-29	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin