coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
* \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/ /
* \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\| *	Add corresponding field in `VernacInductive`.	Arnaud Spiwack	2015-06-24
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Rework typeclass resolution and control of backtracking.	Matthieu Sozeau	2014-09-15
*	Remove [Infer] option of records.	Arnaud Spiwack	2014-09-04
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Updating headers.	herbelin	2012-08-08
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	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
*	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
*	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack	2009-01-19
*	DISCLAIMER	puech	2009-01-17
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
*	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau	2008-11-10
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack	2008-11-05
*	Fixes in handling of implicit arguments:	msozeau	2008-07-04
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Nouvelle en-tête	herbelin	2004-07-16
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin	2003-09-06
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin	2002-06-03
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Utilisation des de Bruijn pour la constructions des records et de leur projec...	herbelin	2002-05-13
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	entetes	filliatr	2001-03-15
*	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin	2001-02-14