The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I am confused about how Coq's backtracking works when there are multiple 
subgoals tied together by existential variables.  In such cases, there 
may be multiple solutions to a subgoal, but only a subset of those allow 
other subgoals to be solved.  However, it seem like Coq's backgracking 
during tactic automation (eauto, for example) doesn't take this into 
account, and instead refuses to let backtracking undo a solved subgoal 
in order to try a different solution.

Is that true?  If not, how does one coerce automation like eauto to 
attempt such alternate subgoal solutions?  Or, if it is true, is there 
something else in the tactic language that can be used to drive such 
alternative-solution attempts when existential variables are present?

Thanks in advance,
Jonathan