coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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