The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2014-07-02 11:07 GMT+02:00 Julien Narboux 
<jnarboux AT narboux.fr>:
> There is a command "Show intros" to display the names which will be
> generated. It is possible to build a script which replace intros. intos
> named intros, a good starting point for writing such a script could be the
> one for indenting writen by Eelis:
> https://github.com/jnarboux/corn/blob/master/tools/coqindenter

Hi, great idea to have such a script.

In proofgeneral I implemented something related to this: the 'smart
intros' command which (by using Show Intros) automatically inserts a
named intros in the script. But this is to be used when developing
your script, not afterward (although it could probably be adapted). It
could be a feature wish for coqide.

Default shortcut: C-c C-a C-i (M-x coq-insert-intros).

P.

> We could have also an option to prevent you from using automatically named
> variables (the prefix could be something like a utf8 character for space). I
> think this is the default behaviour in Isabelle/Isar.

This is also in ssreflect.