Frédéric Blanqui

It would be nice to have in emacs/vscode shortcuts/menus to run some commands (compute, type, print, search, flag, debug, verbose) without having to write them in the file.

In Stdlib.List: ``` opaque symbol rot_size [a] (l:𝕃 a) : π (rot (size l) l = l) ≔ begin assume a l; simplify; rewrite take_size l; rewrite @drop_size; reflexivity; end;...

In Stdlib.List: ``` opaque symbol rot_size [a] (l:𝕃 a) : π (rot (size l) l = l) ≔ begin assume a l; simplify; rewrite take_size l; flag "print_implicits" on; rewrite...

In this example, lambdapi get stucked in the Term.cleanup of a definition after the end of the definition (pdata_finalize). [blockedproof.tar.gz](https://github.com/user-attachments/files/17691817/blockedproof.tar.gz)

man rocq provides almost no information

1

### Description of the problem `man rocq` does not list the subcommands and provides a wrong URL. ``` ROCQ(1) General Commands Manual ROCQ(1) NAME rocq - The Rocq Prover SYNOPSIS...

improve applicability of the apply tactic

2

In various cases, apply fails and one needs to instead use refine with various underscores. This PR tries to make apply works more often.