I’m trying to use Coq with Proof General, but I’m new to this and don’t know what I’m doing.
I installed Coq on my Mac and was able to use CoqIDE.
Then I installed Emacs and Proof General, but Proof General cannot find coqtop. When I ran
on Terminal, it said “coqtop not found”. How can I fix this? I tried adding
(setq coq-prog-name “/usr/bin/coqtop -emacs”)
to my .emacs but it didn’t help.