coq - The formal proof system

Age	Commit message (Expand)	Author
2009-02-06	Fixing #2044 (bad printing of primitive notation at the head of	herbelin
2009-01-19	The initial state evar numbering increased. Fix output message in a test.	puech
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2009-01-02	Regression test for bug #1967	herbelin
2009-01-02	Conséquence renommage canonique de refl_equal en eq_refl.	herbelin
2008-12-02	Miscellaneous fixes and improvements:	herbelin
2008-11-27	Test case for previous commit.	msozeau
2008-11-09	- Correction erreur dans test output Notation.v	herbelin
2008-11-07	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin
2008-10-28	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-22	Affichage des notations récursives:	herbelin
2008-08-05	Correction de bugs:	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-29	Oops... the trunk behaviour is different	glondu
2008-07-29	Update test-suite output	glondu
2008-07-01	Documentation Prop<=Set et Arguments Scope Global	herbelin
2008-06-05	Renommage id dans le test Nametab (suite ajout d'une constante de ce	herbelin
2008-04-28	Petites corrections vis à vis des commits 10860, 10859, 10850	herbelin
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2008-03-26	Diverses petites modifs dans la test-suite:	notin
2008-03-25	Correction de bugs relatifs a la compostion des substitutions	soubiran
2008-03-08	Fix bugs that were reopened due to the change of setoid	msozeau
2008-02-01	Beaoucoup de changements dans la representation interne des modules.	soubiran
2008-01-22	Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)	notin
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-07-23	removed thesis	barras
2007-07-12	Update (test-suite was not successful).	glondu
2007-07-02	Factorisation des paramètres dans l'affichage des inductifs	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-13	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin
2006-12-12	MAJ	herbelin
2006-10-13	Correction test-suite suite à r9186	notin
2006-10-09	Exemple avec liaison des variables de filtrage du match	herbelin
2006-10-09	Notations:	herbelin
2006-09-25	Corrections mineures	notin
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-06-09	Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...	herbelin
2006-05-28	Adaptation au passage de sig2 dans Type	herbelin
2006-05-10	Conformité nouveaux principes: Declare Module non utilisable pour définir u...	herbelin
2006-04-24	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin
2006-01-11	Ajout test notation récursive	herbelin
2006-01-05	Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion	herbelin
2006-01-02	Affichage de 'O' (lettre) comme '0' (chiffre)	herbelin
2005-12-23	Test printing of Tactic Notation which was broken until dec 2005	herbelin
2005-12-22	Abandon tests syntaxe v7 (correction)	herbelin
2005-12-22	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin