coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Do not compute constr matching context if not used.	Pierre-Marie Pédrot	2018-04-10
\| \| \| \|	This mitigates bug #6860.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
\| \| \| \|	And some code simplification.
*	Remove up-to-conversion matching functions.	Pierre-Marie Pédrot	2017-12-09
\| \| \| \|	They were not used anymore since the previous patches.
*	[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.
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\| \| \| \| \|	To this extent we factor out the relevant bits to a new file, ltac_pretype.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Constr_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
\| \| \| \| \| \|	Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables.
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Avoiding introducing yet another convention in naming files.	Hugo Herbelin	2015-01-08