Dear Coq users,
I'm using Proof General on emacs, and facing a problem. If I do "proof-assert-next-command-interactive"
C-c C-n after using "I-search"
C-s, then the proof process gets stuck and never ends. Does anyone experienced the same problem? I hope to get some tips to fix it.
I use macOS Big Sur, GNU Emacs 27.1, Proof General Version 4.5-git, Company-Coq.
Dear @Yosuke Ito , I have no such problem, seems strange. Emacs is a bit tricky due to user-config, I'd suggest you report the issue at https://github.com/ProofGeneral/PG/issues where they should be able to help you debug it
OK. I'll send a bug report. Thank you very much for your help!
Last updated: Feb 06 2023 at 11:03 UTC