coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	Rewrite sort_universes to minimize the number of universes	glondu	2011-01-25
*	In univ.ml, put universe_level primitives in its their own sub-module	glondu	2011-01-11
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	More coherent comment ordering	glondu	2011-01-11
*	Univ: try to avoid a few lookup in the universe graph	letouzey	2010-12-18
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Revert last commit 13723 on Univ : minor gains and more complex code	letouzey	2010-12-18
*	Univ: an attempt to lazily compact chains of Equiv in a functionnal way	letouzey	2010-12-17
*	Univ: two improvements (speed + space)	letouzey	2010-12-16
*	In Univ, unify order_request and constraint_type	glondu	2010-11-03
*	More generic Univ.dump_universes	glondu	2010-11-02
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)	herbelin	2010-04-20
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)	letouzey	2008-11-16
*	Correct display of constraints for Print Universes "dumpfile"	letouzey	2008-11-15
*	Faster comparison of universes	letouzey	2008-11-14
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...	soubiran	2008-06-06
*	Changement de stratégie vis à vis du commit 10859 sur la gestion des	herbelin	2008-05-12
*	Correction du bug des types singletons pas sous-type de Set	herbelin	2008-04-27
*	added the .vo checker (with independent Makefile)	barras	2008-04-21
*	Application de refresh_universes dans typing.ml et retyping.ml : les	herbelin	2008-03-15
*	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack	2007-12-18
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Prise en compte des univers algébriques dans les types inférés dans	herbelin	2007-01-19
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	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