coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès	2018-03-09
\|\
\| *	Pass the constant cache as a separate argument in kernel reduction.	Pierre-Marie Pédrot	2018-03-04
\| \|
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \| \| \| \|	No using a mutable counter to skip them, instead we keep them in the environment.
*	Fix reduction flags in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \| \| \| \| \|	The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters.
*	inferCumulativity: add comment to explain [if not is_arity].	Gaëtan Gilbert	2018-02-11
\|
*	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
	This ensures by construction that we never infer constraints outside the variance model.