index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
coretactics.ml4
Age
Commit message (
Expand
)
Author
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