При использовании элемента auto или eauto из Try Tactics CoqIde отвечает следующим сообщением независимо от того, где находится текущая позиция:
Currently, the parsing api only supports parsing at the tip of the document.
You wanted to parse at: 0 but the current tip is: 54
Что не такздесь