coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-04-28	r8931@thot: notin \| 2006-04-28 16:19:38 +0200	notin
2006-04-28	Typo dans précédent commit (8755); protection renforcée dans analyse claus...	herbelin
2006-04-27	- Distinction explicite des parties paramètres et arguments dans le type	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-27	préparation de add_glob en vue d'isolement de la partie module pour	herbelin
2006-04-26	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin
2006-04-24	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-04-07	- Documentation of the Program tactics.	msozeau
2006-03-31	Amendement impression evar pour affichage des Meta par 'info'	herbelin
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-03-22	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-03-04	Correction message d'erreur ltac et adoption du modèle de message de Tacinterp	herbelin