coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing simple induction / destruct from the AST.	Pierre-Marie Pédrot	2014-08-07
*	Instead of relying on a trick to make the constructor tactic parse, put	Pierre-Marie Pédrot	2014-08-07
*	Removing the "constructor" tactic from the AST.	Pierre-Marie Pédrot	2014-08-07
*	Removing "intros untils" from the AST.	Pierre-Marie Pédrot	2014-08-06
*	Removing some tactic compatibility layer.	Pierre-Marie Pédrot	2014-08-01
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	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
*	Moving the "specialize" tactic out of the AST. Also removed an obsolete	Pierre-Marie Pédrot	2014-05-22
*	Moving left & right tactics out of the AST.	Pierre-Marie Pédrot	2014-05-21
*	Moving (e)transitivity out of the AST.	Pierre-Marie Pédrot	2014-05-20
*	Tactics declared through TACTIC EXTEND that are of the form	Pierre-Marie Pédrot	2014-05-20
*	Tentative to add constr-using primitive tactics without grammar rules.	Pierre-Marie Pédrot	2014-05-20
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16