coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
*	diverses fonctions ajoutees	filliatr	1999-12-01
*	fin Recordops, et debut Evarutil	filliatr	1999-11-27
*	ajouts divers pour module Printer	filliatr	1999-11-26
*	Backtrack sur modif Evd.evd_concl	herbelin	1999-11-25
*	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
*	- documentation repertoire proofs/	filliatr	1999-10-20
*	module Logic	filliatr	1999-10-14
*	- re-introduction d'une evar_map dans unsafe_env	filliatr	1999-10-13
*	deplacements des var. ex. hors du noyau	filliatr	1999-10-08
*	- un effort sur la doc (ocamlweb)	filliatr	1999-09-19
*	affichage des erreurs de typage dans minicoq	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
*	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
*	mise en place programmation literaire (generation de doc/coq.tex)	filliatr	1999-08-19
*	module Reduction (debut)	filliatr	1999-08-18
*	generic, term et evd	filliatr	1999-08-17