aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactic_option.ml
AgeCommit message (Collapse)Author
2010-03-05Add a generic tactic option builder. Use it in firstorder to set themsozeau
default solver (using "Set Firstorder Solver") and for program's obligation tactic. I don't understand exactly the reason of the warning when building states/initial.coq, anyone? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7