coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-10	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-29	Multiples changements autour des implicites :	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-13	Correction bug #1477 sur ordre des variables partagées par les or-patterns.	herbelin
2007-03-28	Support for implicit formal argument types in Program ; parse types in type s...	msozeau
2007-03-20	Correction bug affichage des notations des noms de fonctions appliquées	herbelin
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-02-24	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-07	Correction bug #1364 (les variables de section sont repérées par	herbelin
2007-01-22	Allègement de l'affichage des références par le printer si possible	herbelin
2007-01-11	Ajout d'une option de débogage pour expliciter l'instance des evars	herbelin
2007-01-10	Suite commit restructuration discharge (application du type de	herbelin
2007-01-10	Nouvelle approche pour le discharge modulaire	herbelin
2006-12-23	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau
2006-12-12	Variable print_instances pour dÃ©boguer les instances d'evar	herbelin
2006-12-08	Pas d'escamotage des noms rÃ©servÃ©s si Set Printing All actibvÃ©	herbelin
2006-12-03	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin
2006-11-20	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin
2006-10-23	Add a flush for a warning.	courtieu
2006-10-09	Notations:	herbelin
2006-10-06	Annulation de l'essai de changement de sémantique du %scope (révision 9208).	herbelin
2006-10-05	Essai de changement de sémantique du %scope :	herbelin
2006-09-24	Tentative d'amélioration du message d'erreur en cas de paramètre non laissé	herbelin
2006-09-24	Correction bug dans détection clause "in" mal formée quand le "in" est	herbelin
2006-09-23	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin
2006-09-23	- Correction filtrage des notations impliquant un "match" : la présence	herbelin
2006-09-22	Protection List.fold_left2 (cf bug #1224)	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-01	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin
2006-07-07	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin
2006-07-03	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin
2006-06-23	documentation	herbelin
2006-06-22	Légère mise à jour	herbelin
2006-06-22	Added {measure x f} as a valid recursion order.	msozeau
2006-06-08	Changement du type d'argument 'TacticArgType X' en un type	herbelin
2006-06-08	Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...	notin
2006-06-07	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-05-28	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin
2006-05-24	Adaptation de Coqdoc au nouveau add_glob	notin
2006-05-23	Retour version 8852 de constrintern.ml	herbelin
2006-05-23	Erreur commit constrintern.ml	herbelin
2006-05-23	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin
2006-05-23	Modification de add_glob (support des modules dans Coqdoc)	notin
2006-05-19	Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort	herbelin