Help wanted understanding Menhir parser

Yes, one should always have an explicit “end of stream” token (lets call it ξ) generated by one’s lexical analyzer, and one’s initial production S can always be replaced by a new production S' → S ξ which is made the new initial production. That is generally necessary in most parsing systems.