coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added the automatic generation of the boolean equality if possible and the	vsiles	2007-10-05
*	Correction de quelques défauts d'affichage (notations sous "as" pour	herbelin	2007-10-05
*	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin	2007-09-21
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin	2007-08-29
*	dead code	letouzey	2007-07-11
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	More natural notation for intro pattern: @a -> ?a	glondu	2007-07-09
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	Fix bug in subst_cases_pattern when aliasing recursive notations.	msozeau	2007-07-02
*	Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record	herbelin	2007-06-30
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin	2007-05-10
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin	2007-04-28
*	Correction bug #1477 sur ordre des variables partagées par les or-patterns.	herbelin	2007-04-13
*	Support for implicit formal argument types in Program ; parse types in type s...	msozeau	2007-03-28
*	Correction bug affichage des notations des noms de fonctions appliquées	herbelin	2007-03-20
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin	2007-02-24
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Correction bug #1364 (les variables de section sont repérées par	herbelin	2007-02-07
*	Allègement de l'affichage des références par le printer si possible	herbelin	2007-01-22
*	Ajout d'une option de débogage pour expliciter l'instance des evars	herbelin	2007-01-11
*	Suite commit restructuration discharge (application du type de	herbelin	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	Variable print_instances pour dÃ©boguer les instances d'evar	herbelin	2006-12-12
*	Pas d'escamotage des noms rÃ©servÃ©s si Set Printing All actibvÃ©	herbelin	2006-12-08
*	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin	2006-12-03
*	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin	2006-11-20
*	Add a flush for a warning.	courtieu	2006-10-23
*	Notations:	herbelin	2006-10-09
*	Annulation de l'essai de changement de sémantique du %scope (révision 9208).	herbelin	2006-10-06
*	Essai de changement de sémantique du %scope :	herbelin	2006-10-05
*	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-24
*	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-23
*	Protection List.fold_left2 (cf bug #1224)	herbelin	2006-09-22
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin	2006-09-01
*	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin	2006-07-07
*	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin	2006-07-03
*	documentation	herbelin	2006-06-23
*	Légère mise à jour	herbelin	2006-06-22
*	Added {measure x f} as a valid recursion order.	msozeau	2006-06-22
*	Changement du type d'argument 'TacticArgType X' en un type	herbelin	2006-06-08