coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing Pervasives.equality in extraction.	Pierre-Marie Pédrot	2014-03-03
*	Specializing hash functions for widely used types.	ppedrot	2013-10-24
*	Universe counters on slaves are in sync with master	gareuselesinge	2013-08-20
*	A version of Univ.check_eq with no anomaly for Evd.set_eq_sort	letouzey	2013-03-12
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of dir_path	ppedrot	2012-12-14
*	Small cleaning of interface in Univ	ppedrot	2012-11-26
*	univ inconsistency error message gives evidence of a cycle	barras	2012-10-17
*	Updating headers.	herbelin	2012-08-08
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Univ: a univ_depends function to avoid a hack in Inductiveops	letouzey	2012-03-01
*	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey	2011-10-26
*	Hash-consing of mutual_inductive_body (and Univ.constraints)	letouzey	2011-10-10
*	Hash-consing of constr could share more	letouzey	2011-10-02
*	Fix the hconsing of universes	letouzey	2011-09-07
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	More coherent comment ordering	glondu	2011-01-11
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	In Univ, unify order_request and constraint_type	glondu	2010-11-03
*	More generic Univ.dump_universes	glondu	2010-11-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	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	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	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
*	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack	2007-12-18
*	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
*	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
*	Code v7 obsolete	herbelin	2005-05-05
*	Nouvelle en-tête	herbelin	2004-07-16
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	GROS COMMIT:	barras	2001-11-05
*	Nettoyage des commentaires	herbelin	2001-09-20
*	Passage aux univers algébriques	herbelin	2001-09-09
*	Ajout hashconsing univers	herbelin	2001-07-03
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12