coq - The formal proof system

Age	Commit message (Expand)	Author
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
2003-01-26	all tactics should be covered now: remains	bertot
2003-01-25	Add translations for many tactics but a dozen are still remaining	bertot
2003-01-24	Inspect does not work for pcoq and there is no simple fix because inspect	bertot
2003-01-24	The data constructed when detecting an error in a list of commands must	bertot
2003-01-24	Corrects the way conjunctions, existential quantifications, and arrows are	bertot
2003-01-23	Make sure proof by pointing works.	bertot
2003-01-23	Make proof by pointing work for the new notations of existential quantification.	bertot
2003-01-23	oubli des add_recursors singleton logiques	letouzey
2003-01-23	maj V7.4	letouzey
2003-01-22	MAJ	herbelin
2003-01-22	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot
2003-01-22	petit bug pp haskell	letouzey
2003-01-22	Extraction des modules, enfin !	letouzey
2003-01-21	Make sure pcoq will also display hypotheses with a value.	bertot
2003-01-21	Add a few operators in the new version of xlate.ml and make sure	bertot
2003-01-20	Utilisation de 'Recursive' pour les tactiques récursives	herbelin