coq - The formal proof system

Age	Commit message (Expand)	Author
2007-12-31	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-12-06	Commit intermédiaire express de réparation de coqide.ml, que j'avais	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-11-08	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin
2007-10-05	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-09-21	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin
2007-09-06	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin
2007-08-29	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin
2007-07-11	dead code	letouzey
2007-07-11	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey
2007-07-09	More natural notation for intro pattern: @a -> ?a	glondu
2007-07-06	New intro pattern "@A", which generates a fresh name based on A.	glondu
2007-07-02	Fix bug in subst_cases_pattern when aliasing recursive notations.	msozeau
2007-06-30	Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record	herbelin
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