coq - The formal proof system

Age	Commit message (Expand)	Author
2001-06-25	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin
2001-06-19	Extension des parametres de Clear + Inst	delahaye
2001-06-18	Interpretation MetaId + Progress + Inst	delahaye
2001-06-11	Fix de quelques bugs syntaxiques de Ltac	delahaye
2001-04-24	Les clauses de Rec doivent prendre des tactic_atom's	delahaye
2001-04-20	Petit menage	delahaye
2001-04-19	* empty log message *	mayero
2001-04-19	Essais dans Ltac	delahaye
2001-04-14	Non parenthesage des applications de tactiques	delahaye
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-03-15	entetes	filliatr
2001-02-16	Prise en compte noms longs dans SuperAuto	herbelin
2001-02-07	Modif pour les patterns de sous-termes	delahaye
2001-02-01	* empty log message *	mohring
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-20	ajout ident_or_constrarg pour NewInduction	herbelin
2000-12-19	Correction associativite de Repeat/Orelse	delahaye
2000-12-11	numarg -> pure_numarg a poursuivre	mohring
2000-12-06	Extension de la syntaxe de LetTac	herbelin
2000-12-06	Correction pour les qualidconstarg	delahaye
2000-12-05	Plus de quote devant les ident et les ?	delahaye
2000-11-28	Elimination du '	delahaye
2000-11-26	Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...	herbelin
2000-11-23	Bug qualidconstarg (intervient pour Transparent)	herbelin
2000-11-20	Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT pou...	herbelin
2000-11-03	compilation des fichiers ml4 sans GNUseries	filliatr
2000-10-30	Priorite du Try/Orelse + Debug switch + correction bug dans Pattern	delahaye
2000-10-03	Ajout castedopenconstrarg; Renommage tactique Let en LetTac	herbelin
2000-08-17	Pattern matching de sous-termes + exceptions dans le lexer	delahaye
2000-07-21	Modifs d'interpretation de patterns + exceptions dans le lexer	delahaye
2000-05-03	Ajout du langage de tactiques	delahaye
2000-01-26	Fin du changement comarg -> constrarg	herbelin
2000-01-13	Nettoyage des fichiers de parsing	herbelin
2000-01-07	Renommage command en constr	herbelin
1999-12-13	- états fabriqués avec -silent	filliatr
1999-12-02	modifs pour premiere edition de liens	filliatr
1999-09-08	compilation des grammaires (ouf)	filliatr
1999-09-08	modules grammaire Coq	filliatr