Set Firstorder Solver idtac. about coqtail HOT 1 CLOSED

The problem is the current solution of trying to guess the option value's type is pretty fragile. A better solution would be to get a list of all options and their types from Coq, but neither the GetOptions XML command nor Print Options seems to include Firstorder Solver. Two potential workarounds are to hardcode special cases for options that take tactic arguments (are there others?), or pass the whole command with Add instead of SetOptions and let Coq figure it out.

I'll take a look at what CoqIDE and VsCoq do and try to address this in the next couple days.

from coqtail.