PG icon indicating copy to clipboard operation
PG copied to clipboard

Use `rocq repl` instead of `coqtop` when available

Open SkySkimmer opened this issue 10 months ago • 1 comments

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.

SkySkimmer avatar Feb 11 '25 11:02 SkySkimmer

Thanks @SkySkimmer . We will try to get something working quickly.

Matafou avatar Feb 27 '25 16:02 Matafou