coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[econstr] Remove some Unsafe.to_constr use.	Emilio Jesus Gallego Arias	2018-06-04
*	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
*	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\
\| *	Remove unused argument to solve_constraints_system	Gaëtan Gilbert	2018-05-17
\| *	Move solve_constraint_system near its only use site (comInductive)	Gaëtan Gilbert	2018-05-17
* \|	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias	2018-05-08
\|/
*	Deprecate mixing univ minimization and evm normalization functions.	Gaëtan Gilbert	2018-04-17
*	Fixing the 3 cases of a "Stream.Error" ended with two periods.	Hugo Herbelin	2018-04-12
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	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