The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

 > Basically, what I would like Coq to do is to perform this resolution only 
 > once,
 > when the goal is originally solved in interactive mode.
 > One way to achieve this would be by designing a vernacular command that
 > would perform the same Prolog-like resolution as Auto but that does not
 > affect the goal,  and instead produces a script that solves the goal.
 > This script could then be played to solve the goal. The script
 > would mainly feature "Intro" and "Apply" tactics, which are compiled very 
 > fast.
 >
 > Maybe there is already a way to do this or something similar,
 > if so please let me know.

"Info Auto" is what you need.

-- 
Jean-Christophe