coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
*	Adding a local type-in-type flag in kernel declarations.	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
\|\
* \|	This is an attempt to clarify terminology in choosing variable names	Hugo Herbelin	2016-04-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\ \
\| * \|	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
* \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\| \|
\| * \|	Fixing bde12b70 about reporting ill-formed constructor.	Hugo Herbelin	2016-01-26
* \| \|	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
* \| \|	Fixing e3cefca41b about supposingly simplifying primitive projections	Hugo Herbelin	2015-12-15
* \| \|	Slight simplification of the code of primitive projection (in relation	Hugo Herbelin	2015-12-05
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\| \|
\| * \|	Fixing fix c71aa6b to primitive projections.	Hugo Herbelin	2015-11-18
\| * \|	Slightly documenting code for building primitive projections.	Hugo Herbelin	2015-11-18
\| * \|	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin	2015-11-18
* \| \|	Merge origin/v8.5 into trunk	Hugo Herbelin	2015-11-10
\|\\| \|
\| * \|	Dead code from the commit having introduced primitive projections (a4043608).	Hugo Herbelin	2015-11-10
\| * \|	Fixing a bug in reporting ill-formed constructor.	Hugo Herbelin	2015-11-10
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\| \|
\| * \|	Fixing a bug in reporting ill-formed inductive.	Hugo Herbelin	2015-10-22
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\| \|
\| * \|	Univs: inductives, remove unneeded test	Matthieu Sozeau	2015-10-14
* \| \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\| \|
\| * \|	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\\| \|
\| * \|	Implementing Herbelin's fix for the "NonPar" bug	mlasson	2015-09-03
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\| \|
\| * \|	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
\| * \|	Kernel: primitive projections handling of let-ins	Matthieu Sozeau	2015-07-09
\| * \|	Template polymorphism: A bug-fix for Bug #4258	mlasson	2015-07-09
\| \| *	Add a corresponding field in `mutual_inductive_entry` (part 2).	Arnaud Spiwack	2015-06-24
\| \| *	Add a corresponding field in `mutual_inductive_entry` (part 1).	Arnaud Spiwack	2015-06-24
\| \| *	Add a field in `mutual_inductive_body` to represent mutual inductive whose po...	Arnaud Spiwack	2015-06-24
\| \|/ \|/\|
* \|	Document the positivity checker.	Arnaud Spiwack	2015-06-23
\|/
*	Fixing computation of non-recursively uniform arguments in the	Hugo Herbelin	2015-03-24
*	Fixing wrong rel_context in checking positivity condition.	Hugo Herbelin	2015-03-24
*	Univs: When computing the level of an inductive including indices, lets	Matthieu Sozeau	2015-02-14
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Fix issue in printing due to de Bruijn bug when constructing compatibility	Matthieu Sozeau	2015-01-13
*	Update headers.	Maxime Dénès	2015-01-12
*	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau	2015-01-05
*	Fix treatment of universe context in typecheck inductive (was added	Matthieu Sozeau	2014-12-15
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
*	Option -type-in-type continued (deactivate test for inferred sort of	Hugo Herbelin	2014-11-19