coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\| \| \| \| \| \|	ML tactics that may be used as simple identifiers are now declared as a true Ltac entry pertaining to the module that contains the Declare ML Module statement.
*	Moving code of tactic interpretation from Tacenv to Vernacentries.	Pierre-Marie Pédrot	2014-08-31
\| \| \| \| \|	This allows to directly register globtactics in the Tacenv API, without having to resort to any internalization function.
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
\| \| \| \| \|	Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
\| \| \| \|	potentially conflicting tactics names from different plugins.
*	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
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
\| \| \| \| \| \| \| \| \|	Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
\| \| \| \| \| \| \| \|	Tactics notation interpretation was messed up because of the use of identical keys for different notations. All my tentative fixes were unsuccessful, so better blankly revert the commit for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
	Instead of putting the body directly in the AST, we register it in a table. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7