coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	REFORMATTING: kernel/context.ml{,i}	Matej Kosik	2016-02-09
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	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
* \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Remove an ununsed pattern and commented code in the kernel.	Matthieu Sozeau	2014-10-24
*	Pushing Pierre's factorization of names in goal context printing from	Hugo Herbelin	2014-10-22
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier	2014-09-01
*	Removing some generic equalities.	ppedrot	2013-10-22
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29