coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	maj	filliatr	2003-04-01
*	Déplacement with_option dans Options	herbelin	2003-04-01
*	Correction bug #261 + amélioration nommage	herbelin	2003-04-01
*	Extension de Replace aux égalités entre preuves	herbelin	2003-04-01
*	Fail 1 pour traverser le match	herbelin	2003-04-01
*	maj	filliatr	2003-04-01
*	MAJ	herbelin	2003-03-31
*	Noms absolus	herbelin	2003-03-31
*	Ajout double_plus	herbelin	2003-03-31
*	Ajout Implicit Variable Type	herbelin	2003-03-31
*	Plus de eqT; message Fail	herbelin	2003-03-31
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Ajout d'un message à FailTac; localisation des appels à des tactiques défi...	herbelin	2003-03-31
*	Mise en place d'un traducteur de noms v7->v8	herbelin	2003-03-31
*	Ajout d'un choix 'onlyparse'	herbelin	2003-03-31
*	Suppression des alias eqT/exT/exT2 en nouvelle syntaxe	herbelin	2003-03-31
*	Ajout VernacReserve et suppression des types re-inferables	herbelin	2003-03-31
*	Restauration de make_all_different (disparu depuis version 1.74) car sinon de...	herbelin	2003-03-31
*	Bug pattern_occ_hyp_list	herbelin	2003-03-31
*	Correcting a bug occuring when the mimicked function had a	courtieu	2003-03-31
*	Notation eqT superflue	herbelin	2003-03-31
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	minus a changé d'emplacement -> omega pas content	letouzey	2003-03-31
*	maj	filliatr	2003-03-31
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	indentation	herbelin	2003-03-29
*	Déplacement de minus dans Peano	herbelin	2003-03-29
*	Implicit Variables Type	herbelin	2003-03-29
*	Implicit Variables Type dans les inductive	herbelin	2003-03-29
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	maj	filliatr	2003-03-29
*	coqide: command window maj.	monate	2003-03-28
*	Pas d'associativité gauche au niveau 3 en vieille syntaxe !	herbelin	2003-03-28
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
*	coqide: bug undo corrige	monate	2003-03-28
*	Réparation bug de l'unification. En effet, avant l'instanciation d'une evar	clrenard	2003-03-28
*	Fixed Relative names not,iff in Camlp4 quotation.	corbinea	2003-03-28
*	coqide: bugfix du C-C pendant Undo+paren_highlight	monate	2003-03-27
*	MAJ des mots-clés, Definition, Theorem, ...	herbelin	2003-03-27
*	MAJ des mots-clés, Definition, Theorem, ...	herbelin	2003-03-27
*	coqide: efficacite des buts etc...	monate	2003-03-27
*	Affinement nommage des productions	herbelin	2003-03-27
*	coqide: locale iso-8859-1 par defaut si probleme. Interdiction des lemmes loc...	monate	2003-03-26
*	coqide: addloadpath corrige	monate	2003-03-26
*	ajout d'une fonction reset_mod	monate	2003-03-26
*	Ajout de Set Print Width	gregoire	2003-03-26
*	maj	filliatr	2003-03-26
*	Extract Constant marche avec les axiomes schémas de types	letouzey	2003-03-25
*	coqide: compact delete event-search start	monate	2003-03-24