coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Inductifs avec polymorphisme de sorte (version initiale)	herbelin	2006-03-29
*	Simplification message d'anomalie	herbelin	2005-09-08
*	Bug affichage graphe univers	herbelin	2005-05-05
*	MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...	herbelin	2005-05-05
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)	barras	2004-10-20
*	Nouvelle en-tête	herbelin	2004-07-16
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	compat ocaml 3.03	filliatr	2001-12-13
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	GROS COMMIT:	barras	2001-11-05
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	Passage aux univers algébriques	herbelin	2001-09-09
*	Parsing	herbelin	2001-08-10
*	Ajout hashconsing univers	herbelin	2001-07-03
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	Changement de la structure des points fixes	barras	2001-05-03
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin	2000-11-28
*	Correction incompatibilites dans la fn des types des inductifs	herbelin	2000-10-06
*	correction bug univers (dummy_univ)	filliatr	2000-10-06
*	ensembles de contraintes d'univers	filliatr	1999-09-25
*	- abstraction	filliatr	1999-08-26