coq - The formal proof system

Age	Commit message (Expand)	Author
2015-03-22	Aliasing give_up with admit	Enrico Tassi
2015-02-10	More expressive API for tclWITHHOLES.	Pierre-Marie Pédrot
2015-02-10	Revert "Removing spurious tclWITHHOLES."	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-12-23	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack
2014-12-16	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot
2014-12-12	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack
2014-10-22	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack
2014-09-02	Removing [revert] tactic from the AST.	Pierre-Marie Pédrot
2014-08-31	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot
2014-08-27	Removing spurious tclWITHHOLES.	Pierre-Marie Pédrot
2014-08-07	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-06	Removing "intros untils" from the AST.	Pierre-Marie Pédrot
2014-08-01	Removing some tactic compatibility layer.	Pierre-Marie Pédrot
2014-06-17	Removing dead code.	Pierre-Marie Pédrot
2014-06-06	Moving the [split] tactic out of the AST.	Pierre-Marie Pédrot
2014-06-02	Removing symmetry from the atomic tactics.	Pierre-Marie Pédrot
2014-05-22	Moving the "specialize" tactic out of the AST. Also removed an obsolete	Pierre-Marie Pédrot
2014-05-21	Moving left & right tactics out of the AST.	Pierre-Marie Pédrot
2014-05-20	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-16	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot