The Coq mailing list

["Lukasz Stafiniak" <l_stafiniak AT hoga.pl>]

Hi,

I know that the use of automaticly generated identifiers (e.g. with
Intros.[ENTER] or with some elimination tactics) is gerous for script
reusage. But I like this feature very much -- it decreases the amount of
typing needed, makes proving / programming "action-oriented". So I often
give names even to nondependent product arguments. Would it be possible,
that the system used also the names from lambda-abstractions? For example,
when eliminating a signature, that a name of predicate's argument was
backpropagated and overrided the name given by dependent product? In case of
multiple predicates, the first one would be used.

Sincerely Yours,
Lukasz




Uwaga! Do koñca sierpnia przed³u¿yli¶my promocje, do pakietów
wielostanowiskowych dok³adamy PenDrive  Sprawd¼:
http://www.mks.com.pl/promocja-mobile.html