On 04/02/2012 07:57 AM, Akim Demaille wrote:
> - leave as is

That doesn't sound right; the index is bad.

> - factor the @def macros to all use no `;'
> - try to keep the `;' in the core of the text,
>   but have it appear without the `;' in the Index.

I'd say whichever's easier -- (2) sounds simpler
but I don't know the details.