coq - The formal proof system

Age	Commit message (Expand)	Author
1999-12-03	- global_reference traite des variables	filliatr
1999-12-02	Modifs suite à intégration de class.ml	herbelin
1999-12-02	... dans toplevel	herbelin
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	Renommage de multcase en cases	herbelin
1999-12-01	Retour dans pretyping	herbelin
1999-12-01	déplacé dans kernel	herbelin
1999-12-01	mise au point Declare et avancee dans Astterm	filliatr
1999-12-01	mise a jour Coercion	filliatr
1999-12-01	- environment -> safe_environment	filliatr
1999-12-01	- Typing -> Safe_typing	filliatr
1999-11-30	inductive_key et constructor_key	herbelin
1999-11-30	ocamlweb	filliatr
1999-11-30	ocamlweb	filliatr
1999-11-29	portage modules Evarconv et Evarutil	filliatr
1999-11-29	portage Astterm (partiellement)	filliatr
1999-11-27	fin Recordops, et debut Evarutil	filliatr
1999-11-26	Pas encore pret	herbelin
1999-11-26	Modification pour faire compiler pretyping.ml qui maintenant compile	herbelin
1999-11-26	Maintenant compilable	herbelin
1999-11-26	Version initiale	herbelin
1999-11-26	module Classops; ajout de fonctions dans Declare en consequence	filliatr
1999-11-25	Des progres dans l'integration	herbelin
1999-11-24	MAJ pour fusion avec pretyping	herbelin
1999-11-24	Versions initiales	herbelin
1999-11-24	Deplace dans parsing	herbelin
1999-11-24	Version initiale	herbelin
1999-11-19	Version préliminaire	herbelin
1999-11-18	pas de grosse banniere; pas de double point-virguke	filliatr
1999-10-24	Traducteur ast -> rawterm	herbelin
1999-10-24	Type ML des termes non prétypés	herbelin
1999-10-13	organisation de trad (entre parsing/ et pretyping/)	filliatr