Stream: Proof General users

Topic: Execute block in Company-Coq


view this post on Zulip sameer gupta (Dec 24 2021 at 01:37):

Hi. M-s-Ret doesn't actually run a block or a line long snippet* in company-coq ,what is the hotkey to execute * ? Googling/ readme didn't help and i am keeping, reading dotel files to find the keybindings as last option

view this post on Zulip Pierre Courtieu (Jan 21 2022 at 14:25):

@sameer gupta can you be more precise? What do you expect to have when pressing M-s-Ret?
By the way did you try Meta-shift-return or meta-super-return. Former is bound to company-coq-insert-match-rule-complex and latter to nothing IIUC.
You can send some command directly to the prover using C-c C-v (then type the command), but as it would desynchronise the coq process and the locked region it is only allowed for innocuous commands (like Print or Show Proof).


Last updated: Mar 28 2024 at 19:02 UTC