sameer gupta (Dec 24 2021 at 01:37): 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
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: Oct 13 2024 at 01:02 UTC