coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\
\| *	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
* \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \| \|/ \|/\|
* \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
*	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert	2018-02-10
*	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17