coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
*	Intégration initiale du Cases	herbelin	1999-12-11
*	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
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
*	poursuite de Vernacentries	filliatr	1999-12-01
*	- environment -> safe_environment	filliatr	1999-12-01
*	Backtrack sur modif Evd.evd_concl	herbelin	1999-11-25
*	MAJ pour fusion avec pretyping	herbelin	1999-11-24
*	modules Indrec, Tacentries, Hiddentac	filliatr	1999-11-23
*	- documentation repertoire proofs/	filliatr	1999-10-20
*	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr	1999-10-18
*	module Logic	filliatr	1999-10-14
*	deplacements des var. ex. hors du noyau	filliatr	1999-10-08
*	ensembles de contraintes d'univers	filliatr	1999-09-25
*	- minicoq : definition inductifs; syntaxe a->b	filliatr	1999-09-07
*	environnement sur	filliatr	1999-08-26
*	mach -> typing; machops -> typeops	filliatr	1999-08-26