coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
* \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\\|
\| *	Granting wish #4048: Locate Ltac prints the source of redefined Ltac.	Pierre-Marie Pédrot	2015-05-15
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Adding a test to check whether two tactic notations conflict.	Pierre-Marie Pédrot	2015-05-11
* \|	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot	2015-01-23
* \|	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot	2015-01-21
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot	2014-12-16
*	Fixing nice printing of error reporting with ml tactics bound to ltac names.	Hugo Herbelin	2014-10-01
*	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot	2014-08-31
*	Moving code of tactic interpretation from Tacenv to Vernacentries.	Pierre-Marie Pédrot	2014-08-31
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Useless keeping of dirpath in tactic aliases.	Pierre-Marie Pédrot	2014-06-30
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09