PG
PG copied to clipboard
Use `rocq repl` instead of `coqtop` when available
With the Coq -> Rocq renaming coqtop is a legacy command. It should be possible to use proof general without it.
Currently if I set coq-prog-name to rocq and coq-prog-args to '("repl" "-emacs") PG will swap the arguments calling rocq -emacs repl which is invalid.
Ideally I should not have to touch coq-prog-args but I guess that would require detecting if the program is rocq or coqtop.
Thanks @SkySkimmer . We will try to get something working quickly.