coq - The formal proof system

Age	Commit message (Expand)	Author
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
2003-01-19	Simplification de Simplify (plus de ())	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2003-01-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2003-01-09	Export M + Module M <: SIG	coq
2003-01-06	SearchAbout	filliatr
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-19	Petit netoyage dans lib	coq
2002-12-19	suppression de l'archive cvs d'un bout de debug	letouzey
2002-12-19	les empty ind et les singletons etaient oublies par add_recursors	letouzey
2002-12-19	simplification de solve_subgoal: n'utilise plus frontier	barras
2002-12-18	stupide inlining des construsteurs	letouzey
2002-12-15	Ajout "Locate Notation"	herbelin
2002-12-15	Evaluation paresseuse de l'affichage du debug	herbelin
2002-12-13	debut de parcours des modules	letouzey
2002-12-13	une branche de case inutile	letouzey
2002-12-12	Ajout du vernac Proof with	gregoire
2002-12-11	Compensation de suppression betaiota de type_of	herbelin
2002-12-10	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin
2002-12-10	Normalisation des types (fait avant dans Typing)	herbelin