coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
*	clarification du code	filliatr	1999-12-14
*	debug discharge et inductifs	filliatr	1999-12-10
*	- environment -> safe_environment	filliatr	1999-12-01
*	- Typing -> Safe_typing	filliatr	1999-12-01
*	portage modules Evarconv et Evarutil	filliatr	1999-11-29
*	Modification pour faire compiler pretyping.ml qui maintenant compile	herbelin	1999-11-26
*	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 Redinfo dans library/ pour les constantes d'élimination	filliatr	1999-10-22
*	modules Evar_refiner et Typing_ev	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
*	modules System, Lib et States	filliatr	1999-09-10
*	- environnements vides	filliatr	1999-09-03
*	ajout des inductifs (sans types singletons pour l'instant)	filliatr	1999-08-30
*	suppression champs inutiles dans constantes et inductifs; verification defini...	filliatr	1999-08-27
*	- abstraction	filliatr	1999-08-26
*	modules Instantiate, Constant et Inductive	filliatr	1999-08-25
*	mach et himsg; typage sans extraction	filliatr	1999-08-24
*	- suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujours	filliatr	1999-08-23
*	machine: execute = typage avec univers	filliatr	1999-08-20
*	module Reduction (fin)	filliatr	1999-08-18
*	module Reduction (debut)	filliatr	1999-08-18