The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Jacques-Henri,

my first reaction when I read your answer was: ok I did look so much at the
trees, that I couldn't see the forst any more (as we say in German). But
thinking a bit more about it, it is not so clear to me why this works. My
assumption was that the LTAC match does a match against the syntax tree of the
proof language. But this doesn't seem to be the case. Is the match statement
handled in a special way? How about matching a if then else if then else if
then else sequence? Assume I want to match all the if conditions against a
certain pattern, and don't know at which position it occurs? Can I use a
similar trick?

I couldn't find a documentation for the exact behaviour of the ltac match in
the reference manual.

Thanks & best regards,

Michael