coq - The formal proof system

Age	Commit message (Expand)	Author
2000-01-07	Restructuration printer et parser	herbelin
2000-01-07	Renommage command en constr	herbelin
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-15	Les inductifs dans Scheme doivent être des ident d'inductifs	herbelin
1999-12-13	- états fabriqués avec -silent	filliatr
1999-12-13	- méthode load sur les Hints	filliatr
1999-12-13	Poursuite intégration du Cases	herbelin
1999-12-12	modules et coqc	filliatr
1999-12-11	Intégration initiale du Cases	herbelin
1999-12-10	bug: enregistrement de vartab au lieu de csttab	filliatr
1999-12-10	- erreurs Pretype	filliatr
1999-12-10	Suppression Rel de rawconstr et correction de bugs d'affichage	herbelin
1999-12-10	debug discharge et inductifs	filliatr
1999-12-09	Ajout des messages d'erreurs de Cases	herbelin
1999-12-09	Bug affichage constructeur	herbelin
1999-12-09	- constantes avec recettes	filliatr
1999-12-09	Discharge (encore bugge)	filliatr
1999-12-07	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr
1999-12-06	Bug iterated_binder	herbelin
1999-12-06	declarations eliminations / debuggae inductifs (debut)	filliatr
1999-12-06	erreurs lexicales	filliatr
1999-12-05	mise au point lexer / debugage PP	filliatr
1999-12-03	compilation native	filliatr
1999-12-03	bug make_strength repare	filliatr
1999-12-03	modules profile, Coqinit et Coqtop (=main)	filliatr
1999-12-03	- global_reference traite des variables	filliatr
1999-12-02	modifs pour premiere edition de liens	filliatr
1999-12-02	affichage classes et coercions	filliatr
1999-12-01	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin
1999-12-01	Ajout des fonctions prpattern et prrawterm	herbelin
1999-12-01	Renommage de g_multiple_case en g_cases	herbelin
1999-12-01	module Egrammar	filliatr
1999-12-01	mise au point Declare et avancee dans Astterm	filliatr
1999-12-01	printers	filliatr
1999-12-01	- environment -> safe_environment	filliatr
1999-12-01	- Typing -> Safe_typing	filliatr
1999-11-29	commentaires supprimmés	filliatr
1999-11-29	portage Astterm (partiellement)	filliatr
1999-11-26	Modification pour faire compiler pretyping.ml qui maintenant compile	herbelin
1999-11-26	module Classops; ajout de fonctions dans Declare en consequence	filliatr
1999-11-26	module Pretty (partiellement)	filliatr
1999-11-26	module Termast	filliatr
1999-11-26	module Printer	filliatr
1999-11-26	module Esyntax	filliatr
1999-11-26	module Extend	filliatr
1999-11-24	MAJ pour fusion avec pretyping	herbelin
1999-11-24	Version initiale	herbelin
1999-10-22	- module Redinfo dans library/ pour les constantes d'élimination	filliatr
1999-10-20	- documentation repertoire proofs/	filliatr
1999-10-13	organisation de trad (entre parsing/ et pretyping/)	filliatr