coq - The formal proof system

Age	Commit message (Expand)	Author
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
2012-04-05	Shortcuts and optimizations of comparisons	xclerc
2012-03-22	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey
2012-03-22	Univ: switch the order of int and dir_path in UniverseLevel.Level	letouzey
2012-03-12	Univ: avoid recording dummy universe constraints u<=u or u=u	letouzey
2012-03-02	Noise for nothing	pboutill
2012-03-01	Univ: a univ_depends function to avoid a hack in Inductiveops	letouzey
2012-03-01	Univ: a better Constraint.compare	letouzey
2012-02-29	Univ: a faster is_leq test used when possible	letouzey
2012-02-27	Univ: correct compare_neq (fix #2703)	letouzey
2011-10-26	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey
2011-10-10	Hash-consing of mutual_inductive_body (and Univ.constraints)	letouzey
2011-10-02	Hash-consing of constr could share more	letouzey
2011-09-22	Hash-consing: attempt to stop hash-consing separately constr in declare.ml	letouzey
2011-09-08	More twicks on hash-consing	letouzey
2011-09-07	Fix the hconsing of universes	letouzey
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-01-25	Rewrite sort_universes to minimize the number of universes	glondu
2011-01-11	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
2010-12-18	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-17	Univ: an attempt to lazily compact chains of Equiv in a functionnal way	letouzey
2010-12-16	Univ: two improvements (speed + space)	letouzey
2010-11-03	In Univ, unify order_request and constraint_type	glondu
2010-11-02	More generic Univ.dump_universes	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-05-09	Added a few informations about file lineages (for the most part in kernel)	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-20	Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-08	Some dead code removal + cleanups	letouzey
2008-11-16	Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)	letouzey
2008-11-15	Correct display of constraints for Print Universes "dumpfile"	letouzey
2008-11-14	Faster comparison of universes	letouzey
2008-07-25	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin
2008-06-06	ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...	soubiran
2008-05-12	Changement de stratégie vis à vis du commit 10859 sur la gestion des	herbelin
2008-04-27	Correction du bug des types singletons pas sous-type de Set	herbelin
2008-04-21	added the .vo checker (with independent Makefile)	barras
2008-03-15	Application de refresh_universes dans typing.ml et retyping.ml : les	herbelin
2007-12-18	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-01-19	Prise en compte des univers algébriques dans les types inférés dans	herbelin