Custom Query – Proof General

Results (124 - 126 of 361)

← 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 →

Ticket	Resolution	Summary	Owner	Reporter
#357	fixed	Feature suggestion: function + binding to insert Coq closing tactics	David Aspinall	Erik Martin-Dorel
Description	I have noticed that Coq closing tactics are defined in `coq-syntax.el`, wisely separated from the others tactics, but not available for insertion. It would be convenient, for example, to have a function `coq-insert-solve-tactic` similar to `coq-insert-tactic`, which would help the user to insert one of these closing tactics. As `[C-c C-a C-c]` and `[C-c C-a C-s]` are already used, I would suggest to bind this new function to something like `[C-c C-a !]` which is probably easier to remember. Kind regards, Erik Martin-Dorel.
#356	fixed	Coq identifiers are unexpectedly colorized	David Aspinall	Erik Martin-Dorel
Description	I have just done a cvs update, and the Coq font lock seems to be broken: when an identifier contain a reserved tactic as a substring, such as `ring_scope`, `simpl_pred` or `Section Predicates.`, it is wrongly colorized (viz. because of `ring`, `simpl` and `red`). Kind regards, Erik Martin-Dorel.
#355	wontfix	Autosend should be re-engaged after C-c C-n	David Aspinall	David Aspinall
Description	In case autosending is interrupted but the user hits C-c C-n, automatic sending should be resumed afterwards. (This is suggested in the user manual but not fully working: currently the user needs to modify the buffer first)

← 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 →