search

whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 34 forks source link

Set Firstorder Solver idtac. #317

Closed andres-erbsen closed 1 year ago

andres-erbsen commented 1 year ago 
Set Firstorder Solver idtac.
(*
There is no flag or option with this name: "Firstorder Solver idtac".
[unknown-option,option]
 *)
whonore commented 1 year ago

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.