coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-22	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey
2012-03-01	Univ: a univ_depends function to avoid a hack in Inductiveops	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-07	Fix the hconsing of universes	letouzey
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-01-11	Add "Print Sorted Universes"	glondu
2011-01-11	More coherent comment ordering	glondu
2010-12-18	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey
2010-11-03	In Univ, unify order_request and constraint_type	glondu
2010-11-02	More generic Univ.dump_universes	glondu
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
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
2007-12-18	Nettoyage de code en vue de la release. Plus de Warning: Unused	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
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-03-29	Inductifs avec polymorphisme de sorte (version initiale)	herbelin
2005-05-05	Code v7 obsolete	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras
2001-09-20	Nettoyage des commentaires	herbelin
2001-09-09	Passage aux univers algébriques	herbelin
2001-07-03	Ajout hashconsing univers	herbelin
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin
2000-10-06	MAJ pr_uni	herbelin
2000-10-06	correction bug univers (dummy_univ)	filliatr
1999-09-25	ensembles de contraintes d'univers	filliatr
1999-09-03	modules Libobject et Summary (partiel)	filliatr
1999-08-30	un petit effort de presentation dans les interfaces	filliatr
1999-08-26	- abstraction	filliatr
1999-08-24	mach et himsg; typage sans extraction	filliatr
1999-08-20	machine: execute = typage avec univers	filliatr
1999-08-18	module Reduction (fin)	filliatr