Hello,

> That is, instead of treating the token set precisely as the
> set of user tokens + eof, menhir is treating eof specially
> and not consistently with other tokens.

As far as Menhir is concerned, there is no special eof token.
The set of tokens is exactly the set of user-defined tokens.
This is true also of ocamlyacc.

Internally, the construction of the automaton uses a pseudo-token,
written #, which stands for the end of the token stream. This token
can appear in conflict explanation messages.

> I'm not sure i fully understand the 'do we need lookahead'
> issue: I would have thought: you need a fetch if your action is 
> shift, and not if it is a reduce.

What you mean is, you need to *consume* one token if your action
is shift, and none if your action is reduce. However, in order to
make a decision (in order to choose between shift and reduce, and
between multiple reduce actions), you sometimes need to *consult*
one lookahead token, without consuming it.

This is necessary only *sometimes*, because, in some states, only
one reduce action is possible, and can be taken without consulting
a lookahead token.

An end-of-stream conflict arises when a state has multiple
actions, some of which are on real tokens, and some of which are
on the pseudo-token #. In that case, one would like to consult
the next token in order to make a decision; however, there is a
possibility that we are at the end of the sentence that we are
trying to recognize, so asking the lexer for one more token might
be a mistake (in your terminology, it might be an overshoot).

Does this clarify things?

-- 
François Pottier
Francois.Pottier@inria.fr
http://cristal.inria.fr/~fpottier/