'How to run SearchAbout snippet in company-coq-tutorial
Running M-x company-coq-tutorial, I'm getting stuck at the following instruction in the tutorial:
(* Run the following snippet, then try typing ‘plus’ *)
SearchAbout eq.
I'm assuming it's supposed to be Search eq. in newer versions of Coq.
How do I "run" this snippet? Does the tutorial want me to go to the line below Search eq. and press C-c C-RET, or is there something else I'm supposed to do?
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|