coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5	herbelin	2007-04-10
*	Some changes to eliminate Hevea warnings.	emakarov	2007-04-10
*	Split refman/headers.tex into headers.sty and headers.hva.	emakarov	2007-04-10
*	Eliminated warning messages from Hevea. Most warning messages were	emakarov	2007-04-10
*	simplier version of tail_plus	letouzey	2007-04-06
*	Mise en place d'un rafinement de compute.	jforest	2007-04-05
*	On n'a plus besoin de compiler les anciens fichiers de functionnal induction ...	jforest	2007-04-05
*	Correction partielle du bug #1388 (augmentation de la taille des code accepte...	jforest	2007-04-05
*	Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...	jforest	2007-04-05
*	Corrected a typo in doc/refman/Setoid.tex.	emakarov	2007-04-04
*	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov	2007-04-02
*	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov	2007-04-02
*	Intégration de la modification suggérée par Michal Moskal (cf msg sur Coq ...	notin	2007-04-02
*	Réparation de NArith/BinPos.v suite au commit #9739	notin	2007-04-02
*	Removed the definition of extensions of apply to equivalences	emakarov	2007-04-01
*	Added the following theorems to BinPos:	emakarov	2007-03-30
*	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov	2007-03-30
*	Modifications dans Makefile:	notin	2007-03-30
*	Changement mineur du comportement de 'rewrite .. in * \|-': si le	notin	2007-03-30
*	Support for implicit formal argument types in Program ; parse types in type s...	msozeau	2007-03-28
*	Modification de la vm:	notin	2007-03-27
*	Make multiple patterns work again with Program while simplifying the code.	msozeau	2007-03-26
*	stupid me: ?f two times in a pattern	letouzey	2007-03-26
*	PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ...	letouzey	2007-03-26
*	Correction des bugs #1455 et #1456	notin	2007-03-22
*	Remove debugging code committed by accident	lmamane	2007-03-22
*	A tentative fix for bug #1455	lmamane	2007-03-22
*	Suppression des sauts de lignes superflus de Show Script (test-suite/output/T...	notin	2007-03-21
*	Correction bug affichage des notations des noms de fonctions appliquées	herbelin	2007-03-20
*	Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...	msozeau	2007-03-20
*	ajout contrib/dp/Dp.vo	filliatr	2007-03-20
*	traces Ergo	filliatr	2007-03-20
*	Forgot to update to new cast	msozeau	2007-03-19
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Un chouia de portabilité en plus et pas de test si pas de bogomips	herbelin	2007-03-19
*	MAJ test complexité pour considérer le cas d'un temps avec un nombre	herbelin	2007-03-17
*	Correction du bug #1441	notin	2007-03-16
*	r11153@tannat: jforest \| 2007-03-16 10:25:55 +0100	jforest	2007-03-16
*	Test de non-régression pour commit 9673	herbelin	2007-03-15
*	Typos	herbelin	2007-03-15
*	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin	2007-03-15
*	Prévention notations récursives sans terminal à gauche et qui font boucler	herbelin	2007-03-15
*	Add destruct_call variant where naming of introduced hypotheses is possible. ...	msozeau	2007-03-15
*	Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...	msozeau	2007-03-14
*	Bug dans Makefile (COQINSTALLPREFIX)	notin	2007-03-14
*	Removed an unnecessary argument (p : positive) in Prect_base.	emakarov	2007-03-14
*	Solve obligation handling bug of trying to solve automatically at Next Obliga...	msozeau	2007-03-13
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13
*	Proof simplification for eq_nat_dec et le_lt_dec: induction over	letouzey	2007-03-12
*	correction du bug 1432	jforest	2007-03-11