aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mllib
Commit message (Expand)AuthorAge
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20