I am fairly new to Emacs in general, and Proof General specifically. I stumbled upon a stackoverflow answer (https://stackoverflow.com/a/41838593) that mentions a shortcut fro extracting a goal into a lemma, but I cannot figure out how to use it. The shortcut should be C-c C-a C-x, (which I understand to be holding control down while typing cax), but nothing happens to the proof I am looking at. Any suggestions for what I could be doing wrong?

did you install Company-Coq? https://github.com/cpitclaudel/company-coq

I think this functionality is only available when you have both Proof General and Company-Coq installed.

Ah, that makes sense, thank you!

It is indeed a company-coq feature. You probably want to try the tutorial once you install it: `M-x company-coq-tutorial`

.

Last updated: Feb 06 2023 at 06:29 UTC