coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	We do up to `Term` which is the main bulk of the changes.
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
\| \| \| \| \| \| \| \| \| \| \| \|	This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
*	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
\|
*	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Evardefine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20
	Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.