coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suppression Rel de rawconstr et correction de bugs d'affichage	herbelin	1999-12-10
*	debug discharge et inductifs	filliatr	1999-12-10
*	Ajout des messages d'erreurs de Cases	herbelin	1999-12-09
*	- constantes avec recettes	filliatr	1999-12-09
*	Discharge (encore bugge)	filliatr	1999-12-09
*	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr	1999-12-07
*	correction bug construct_reference	filliatr	1999-12-07
*	check_correct_par n'etait pas fait au bon endroit	filliatr	1999-12-06
*	declarations eliminations / debuggae inductifs (debut)	filliatr	1999-12-06
*	explicitations erreurs inductifs	filliatr	1999-12-05
*	bug make_strength repare	filliatr	1999-12-03
*	modules profile, Coqinit et Coqtop (=main)	filliatr	1999-12-03
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
*	Retour dans pretyping	herbelin	1999-12-01
*	Avant dans pretyping	herbelin	1999-12-01
*	poursuite de Vernacentries	filliatr	1999-12-01
*	diverses fonctions ajoutees	filliatr	1999-12-01
*	- environment -> safe_environment	filliatr	1999-12-01
*	- Typing -> Safe_typing	filliatr	1999-12-01
*	ocamlweb	filliatr	1999-11-30
*	portage modules Evarconv et Evarutil	filliatr	1999-11-29
*	fin Recordops, et debut Evarutil	filliatr	1999-11-27
*	Modification pour faire compiler pretyping.ml qui maintenant compile	herbelin	1999-11-26
*	Evd vient apres Environ -> id_of_existential expanse	filliatr	1999-11-26
*	ajouts divers pour module Printer	filliatr	1999-11-26
*	typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...	filliatr	1999-11-25
*	Backtrack sur modif Evd.evd_concl	herbelin	1999-11-25
*	MAJ pour fusion avec pretyping	herbelin	1999-11-24
*	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr	1999-11-24
*	modules Indrec, Tacentries, Hiddentac	filliatr	1999-11-23
*	module Wcclausenv	filliatr	1999-11-22
*	module Tactics (debut)	filliatr	1999-11-22
*	module Pattern, Wcclausenv (interface) et Tacticals	filliatr	1999-11-19
*	- module Redinfo dans library/ pour les constantes d'élimination	filliatr	1999-10-22
*	- documentation repertoire proofs/	filliatr	1999-10-20
*	module Clenv (debut)	filliatr	1999-10-20
*	modules Evar_refiner et Typing_ev	filliatr	1999-10-20
*	les variables existentielles contiennent maintenant un environnement (type	filliatr	1999-10-19
*	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr	1999-10-18
*	module Logic	filliatr	1999-10-14
*	module Proof_trees	filliatr	1999-10-14
*	plus de recettes pour les corps des constantes	filliatr	1999-10-13
*	- re-introduction d'une evar_map dans unsafe_env	filliatr	1999-10-13
*	documentation	filliatr	1999-10-13
*	redeplacement des var. ex. dans kernel :-)	filliatr	1999-10-13
*	deplacements des var. ex. hors du noyau	filliatr	1999-10-08
*	ajout des constraintes pendant le chargement d'un module (load)	filliatr	1999-09-27
*	message erreur UI pendant import	filliatr	1999-09-26
*	ensembles de contraintes d'univers	filliatr	1999-09-25