Yosuke Ito (Mar 19 2021 at 12:18): Yosuke Ito (Mar 19 2021 at 12:18):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.
Emilio Jesús Gallego Arias (Mar 19 2021 at 15:14):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
Yosuke Ito (Mar 20 2021 at 00:12):OK. I'll send a bug report. Thank you very much for your help!
Last updated: Oct 13 2024 at 01:02 UTC