coq - the Coq proof assistant

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