coq - The formal proof system

Age	Commit message (Expand)	Author
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-08	Some dead code removal + cleanups	letouzey
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-03-28	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau
2007-12-31	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau
2007-07-16	Generalized CAMLP4USE for pp dependencies	corbinea
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2006-10-03	le parsing du LETIN ne suivait pas la DTD (bug #1237)	herbelin
2006-07-05	Nettoyage code mort	herbelin
2006-06-22	Added {measure x f} as a valid recursion order.	msozeau
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-04-27	- Distinction explicite des parties paramètres et arguments dans le type	herbelin
2006-04-26	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-02-04	Parseur pour la DTD XML de constr et un peu plus pour les arguments de tactiques	herbelin