The Coq mailing list

[Marcus Ramos <mvmramos AT gmail.com>]

Now I understand it. Thanks you all for the replies.

Regards,

Marcus.

2013/6/3 Adam Chlipala <adamc AT csail.mit.edu>

On 06/03/2013 01:22 PM, Marcus Ramos wrote:

I am new here, trying to lean the basics of Coq, and have already successfully
proved a few very simple theorems. However, I can´t manage to find a solution
for the first part of exercise 5.9 of "Interactive Theorem Proving..." (page
124). The solution shows the use of:

intros x [H1 | H1]

Although I understand "intros x" and the other tactics used in the solution, I
have no idea what the meaning of the [H1 | H1] next to it is. I have tried to
find it in the documentation, however without success. Can anyone explain this
to me?

You'll find this information in the manual section for [intros]:
    http://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic28

In general, tactic documentation is easy to find, using the manual's tactic index, which is where I got this link.  (Note that the index points to the entry for [intro], but it's necessary to scroll down further to the full-fledged entry for [intros].)