coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Restructuration des outils pour les inductifs.	herbelin	2000-05-18
*	Ajout d'un strong 'light'	herbelin	2000-05-05
*	Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)	herbelin	2000-05-04
*	Retrait fullmind de inductive_summary pour simplicité	herbelin	2000-04-27
*	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin	2000-04-20
*	Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sort...	herbelin	2000-03-21
*	Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'	herbelin	2000-03-17
*	Ajout du test d'égalité des vecteurs dans convert_forall2.	herbelin	2000-03-08
*	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