coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	Removing the "constructor" tactic from the AST.	Pierre-Marie Pédrot	2014-08-07
*	Code cleaning in Tacenv.	Pierre-Marie Pédrot	2014-07-27
*	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
*	Moving the [split] tactic out of the AST.	Pierre-Marie Pédrot	2014-06-06
*	Removing symmetry from the atomic tactics.	Pierre-Marie Pédrot	2014-06-02
*	Allowing Ltac definitions that may be unusable because of a built-in	Pierre-Marie Pédrot	2014-05-21
*	Moving left & right tactics out of the AST.	Pierre-Marie Pédrot	2014-05-21
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Fix bug#2080: error message on Ltac name clash with primitive tactics	xclerc	2014-01-10
*	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