Menhir + error recovery

Can someone point me to some examples of error recovery (code)?

E. g.

parse recover to
foo=2+" foo=2 by backing off to the nearest “parsable” state
foo="2 foo="2" at the point of parsing error you insert a token that could help (and the end)
foo=[; bar=2 foo=[]; bar=2 (not at the end; after [; it is already known that parsing cannot continue)

Especially the latter one. I can’t quite figure out the puzzle made of Parser.MenhirInterpreter.{pop,resume,offer,input_needed}.