coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...	notin	2007-04-26
*	fin des conclusions multiples	corbinea	2007-04-26
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	(PR#1529)	soubiran	2007-04-25
*	Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création	herbelin	2007-04-25
*	Le configure et le README accordent leurs violons pour exiger ocaml 3.07 (res...	herbelin	2007-04-24
*	MAJ ppc/i386	herbelin	2007-04-24
*	Correction du bug #1496 (ajout de Program Definition et Program Fixpoint aux ...	notin	2007-04-23
*	Fixed some typos.	glondu	2007-04-18
*	debug plus poussé induction dépendante	corbinea	2007-04-18
*	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin	2007-04-18
*	Corrected a LaTeX typo.	emakarov	2007-04-17
*	Correct implementation of undo in obligations handling code, correct some bug...	msozeau	2007-04-17
*	Reorder hook and printing of message, more natural this way.	msozeau	2007-04-17
*	Changed many refman/*.tex files. Put \label and \index commands that immediat...	emakarov	2007-04-17
*	Added the option to set/unset the automatic generation of elimination schemes	vsiles	2007-04-17
*	Rajout du mot Fix dans le printer	vsiles	2007-04-17
*	Retablissement de Fix dans print_pure_constr	vsiles	2007-04-17
*	Correction du bug #1510	notin	2007-04-17
*	Export de simplest_eapply, utilisé dans la contrib interface	notin	2007-04-16
*	fix bug with dependent inductive families	corbinea	2007-04-16
*	Add the possibility to change the position of tabs in main window (from r9717).	glondu	2007-04-16
*	Fix a bug which sometimes made coqide crash after changing	glondu	2007-04-16
*	Removed from headers.hva the code to make index point to the section	emakarov	2007-04-16
*	Suite unification apply et eapply (l'un et l'autre profite maintenant	herbelin	2007-04-16
*	Essai de partage de code entre apply et eapply	herbelin	2007-04-15
*	Ajout d'un test de complexité de injection (cf bug 1173)	herbelin	2007-04-14
*	Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,	herbelin	2007-04-14
*	Correction bug #1499	notin	2007-04-13
*	Proposition de correction pour le bug #1173 (ou du moins pour un	herbelin	2007-04-13
*	Correction bug #1477 sur ordre des variables partagées par les or-patterns.	herbelin	2007-04-13
*	Test non régression bug #1491	herbelin	2007-04-13
*	Correction bug #1491	herbelin	2007-04-13
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	Transparency of Z_lt_le_dec	notin	2007-04-12
*	Cleaned doc/common/title.tex file. Increased the space under headers	emakarov	2007-04-12
*	Standardisation format biblio	herbelin	2007-04-12
*	Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a	herbelin	2007-04-11
*	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