coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Merge PR#696: Trunk+cleanup constr of global	Maxime Dénès	2017-06-01
\|\
* \|	Adding "epose", "eset", "eremember" which allow to set terms with	Hugo Herbelin	2017-05-30
* \|	Adding "eassert", "eenough", "epose proof", which allow to state	Hugo Herbelin	2017-05-30
\| *	Ltac cleanup: no more constr_of_global calls	Matthieu Sozeau	2017-05-29
\|/
*	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
*	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
*	[location] Use located in tactics.	Emilio Jesus Gallego Arias	2017-04-24
*	[location] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
*	Attempt to improve error message when "apply in" fail.	Hugo Herbelin	2017-03-15
*	Merge PR#395: Allow hintdb to be parameters in a Ltac definition or	Maxime Dénès	2017-02-27
*	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17