coq - The formal proof system

Age	Commit message (Expand)	Author
2003-05-13	Notations arithmetiques	herbelin
2003-05-08	bugfixes in Ground.	corbinea
2003-05-07	Enhancement of the Ground tactic, addition of GTauto and GIntuition.	corbinea
2003-04-28	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin
2003-04-28	bug concernant les projecteurs de Record avec args logiques	letouzey
2003-04-28	adaptation a Acc_iter	letouzey
2003-04-26	bugfix in Ground tactic	corbinea
2003-04-25	Added the Ground tactic.	corbinea
2003-04-17	Divers	herbelin
2003-04-17	Ajout "at next level" dans Notation	herbelin
2003-04-17	commentaires	herbelin
2003-04-17	Ooops	letouzey
2003-04-17	temporaire	letouzey
2003-04-16	BIG MAJ Extraction:	letouzey
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