The Coq mailing list

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

Hi,

Is the Ltac language going to be enlarged?
If so, I have some suggestions:

 - identifiers generation: concatenating two identifiers
   to get a new identifier; generating a
   fresh (free) identifier from given one by adding
   a numeric postfix

 - accessing the type of a term (e.g. hypothesis identifier),
   by a construct "Match Typeof t With"

 - modifiable containers in the environment, so that user
   tactics could have their own hint bases, and a way to iterate
   over them

Best wishes,
Lukasz Stafiniak




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