The Coq mailing list

[Florian Haftmann <florian.haftmann AT informatik.tu-muenchen.de>]

Hi Taral,

> Set Ltac Debug.
> 
> This will show you the actual environment under which your "using ..."
> clause is being run. It is *not* the same as the (full) environment
> you get with "escape".

indeed it works the following way:

thus (S q + s = n) by n_Sr, plus_Sn_m, qsr.

The rule plus_Sn_m has to named explicitly.

Thanks a lot!
        Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature