coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Vernacinterp et Vernacentries (partiellement)	filliatr	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 Macros et Tacinterp	filliatr	1999-10-22
*	- 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
*	module Refiner	filliatr	1999-10-19
*	les variables existentielles contiennent maintenant un environnement (type	filliatr	1999-10-19
*	mise en place module Refiner	filliatr	1999-10-18
*	- 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
*	- re-introduction d'une evar_map dans unsafe_env	filliatr	1999-10-13
*	redeplacement des var. ex. dans kernel :-)	filliatr	1999-10-13
*	module Logic (ne compile pas encore)	filliatr	1999-10-08
*	deplacement des var. ex. dans proofs	filliatr	1999-10-08
*	quelques trucs necessaires au toplevel	filliatr	1999-09-28