aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactic_option.mli
Commit message (Expand)AuthorAge
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05