coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout destApplication	herbelin	2000-03-07
*	MAJ ocaml 2.99 (espaces dans la syntaxe des cast)	herbelin	2000-01-26
*	MAJ commentaires	herbelin	2000-01-26
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
*	Intégration initiale du Cases	herbelin	1999-12-11
*	debug discharge et inductifs	filliatr	1999-12-10
*	Ajout des messages d'erreurs de Cases	herbelin	1999-12-09
*	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
*	- 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
*	mise en place commandes minicoq	filliatr	1999-09-07
*	- 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