coq - The formal proof system

Age	Commit message (Expand)	Author
2002-05-30	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-10	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin
2002-03-19	Ajout de l'entrée ne_constrarg_list	delahaye
2002-03-17	Meilleure gestion de la reduction dans Field	delahaye
2001-12-13	compat ocaml 3.03	filliatr
2001-09-20	Transparent	barras
2001-08-10	Parsing	herbelin
2001-08-06	Nouvelle entrée ident_or_numarg	herbelin
2001-06-25	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin
2001-06-18	Interpretation MetaId + Progress + Inst	delahaye
2001-04-14	Non parenthesage des applications de tactiques	delahaye
2001-04-09	Uniformisation des 'Save def_tok id'	herbelin
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-04-04	adding entry points for the arguments of the Comment command.	bertot
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-02-16	Prise en compte noms longs dans SuperAuto	herbelin
2001-01-30	backtrack sur le lexeur de la V6	filliatr
2001-01-19	Réparation bug extensibilité de Constr.pattern	herbelin
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-20	ajout ident_or_constrarg pour NewInduction	herbelin
2000-12-16	Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite	herbelin
2000-12-06	Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le b...	herbelin
2000-11-26	Restruration autour de qualidarg	herbelin
2000-11-20	Ajout diverses entrées pour les noms qualifiés	herbelin
2000-11-03	compilation des fichiers ml4 sans GNUseries	filliatr
2000-10-18	2ème	herbelin
2000-10-18	Mise en place de parseurs avec globalisation pas seulement dans les quotation...	herbelin
2000-10-03	Ajout castedopenconstrarg	herbelin
2000-08-17	Pattern matching de sous-termes + exceptions dans le lexer	delahaye
2000-07-28	Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...	herbelin
2000-07-26	bug token "<:" et ":<"	herbelin
2000-06-21	$BINDER -> BINDER	filliatr
2000-05-03	Ajout du langage de tactiques	delahaye
2000-01-26	Fin du changement comarg -> constrarg	herbelin
2000-01-20	Bête renommage	herbelin
2000-01-13	Nettoyage des fichiers de parsing	herbelin
2000-01-07	Restructuration printer et parser	herbelin
1999-12-01	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin
1999-09-08	compilation des grammaires (ouf)	filliatr
1999-09-08	modules Ast et Pcoq	filliatr