coq - The formal proof system

Age	Commit message (Expand)	Author
2003-04-11	Ajout option 'Local' à Infix et Notation	herbelin
2003-04-11	Explicitation arguments de eq	herbelin
2003-04-09	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-07	Mauvaise resolution conflit dans commit precedent	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-04-03	Légères simplifications code de Field; message d'erreur si pas égalité	herbelin
2003-04-01	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-03-31	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-29	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-25	Extract Constant marche avec les axiomes schémas de types	letouzey
2003-03-24	Bugfix pour Linear.	corbinea
2003-03-21	Fin de la résurrection de Linear.	corbinea
2003-03-12	* empty log message *	barras
2003-03-12	* Ajout du traducteur nouvelle syntaxe *	barras
2003-03-11	pour coq-ide	letouzey
2003-03-11	pour ocamlweb	letouzey
2003-03-10	Remove a TODO in the translation of generic arguments:	bertot
2003-03-06	Make sure that identifiers are parsed as qualified identifier and that	bertot
2003-03-01	Added some tests to make more robust the tactique "Functional	courtieu
2003-02-27	Adding tests for the "functional induction" facility.	bertot
2003-02-27	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot
2003-02-25	Suppression des warnings a la compilation de contrib/linear	corbinea
2003-02-24	Bringing Linear back to life (Still somewhat buggy).	corbinea
2003-02-21	bugs/améliorations trouvés via FTA	letouzey
2003-02-05	Ajout du traducteur	desmettr
2003-02-03	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-02	plus d'environment fixe cur_env mais un environment evolutif	letouzey
2003-01-30	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-29	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-28	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