coq - the Coq proof assistant

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