coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Alignement du comportement des implicites d'inductif en sortie de section sur...	herbelin	2003-04-09
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
*	Mauvaise resolution conflit dans commit precedent	herbelin	2003-04-07
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Légères simplifications code de Field; message d'erreur si pas égalité	herbelin	2003-04-03
*	remplace == par = dans la tactique field pour que le debugger marche a nouvea...	narboux	2003-04-01
*	Fail 1 pour traverser le match	herbelin	2003-04-01
*	Noms absolus	herbelin	2003-03-31
*	Plus de eqT; message Fail	herbelin	2003-03-31
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Correcting a bug occuring when the mimicked function had a	courtieu	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
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	Extract Constant marche avec les axiomes schémas de types	letouzey	2003-03-25
*	Bugfix pour Linear.	corbinea	2003-03-24
*	Fin de la résurrection de Linear.	corbinea	2003-03-21
*	* empty log message *	barras	2003-03-12
*	* Ajout du traducteur nouvelle syntaxe *	barras	2003-03-12
*	pour coq-ide	letouzey	2003-03-11
*	pour ocamlweb	letouzey	2003-03-11
*	Remove a TODO in the translation of generic arguments:	bertot	2003-03-10
*	Make sure that identifiers are parsed as qualified identifier and that	bertot	2003-03-06
*	Added some tests to make more robust the tactique "Functional	courtieu	2003-03-01
*	Adding tests for the "functional induction" facility.	bertot	2003-02-27
*	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot	2003-02-27
*	Suppression des warnings a la compilation de contrib/linear	corbinea	2003-02-25
*	Bringing Linear back to life (Still somewhat buggy).	corbinea	2003-02-24
*	bugs/améliorations trouvés via FTA	letouzey	2003-02-21
*	Ajout du traducteur	desmettr	2003-02-05
*	Added a clause for VernacDefineModule, but with an error as result.	bertot	2003-02-03
*	maj status de l'extraction des modules	letouzey	2003-02-03
*	hack horrible pour renommage dans Modules Types et Functeurs	letouzey	2003-02-03
*	encore un long_kn	letouzey	2003-02-03
*	plus d'environment fixe cur_env mais un environment evolutif	letouzey	2003-02-02
*	Auto with zarith essaye Abstract Omega sur un but False	filliatr	2003-01-30
*	fignolage	letouzey	2003-01-30
*	pb d'hier resolu. Recommit	letouzey	2003-01-30
*	apres le backtrack precedent, remise de trois points precis et surs	letouzey	2003-01-29
*	Ca a tout pété -> Bactrack a la version d'hier	letouzey	2003-01-29
*	affichage module et module type	letouzey	2003-01-29
*	affichage module et module type	letouzey	2003-01-29
*	affichage module et module type	letouzey	2003-01-29
*	workaround en attendant traitement reel des modules types	letouzey	2003-01-28
*	amelioration du pretty-print des modules	letouzey	2003-01-28
*	nouvelle gestion des constantes de type	letouzey	2003-01-28
*	all tactics should be covered now: remains	bertot	2003-01-26
*	Add translations for many tactics but a dozen are still remaining	bertot	2003-01-25