The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>]

Hi,

Christophe Dehlinger 
<dehlinger AT dpt-info.u-strasbg.fr>
 wrote:
> 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.
> ...
> Maybe there is already a way to do this or something similar,
> if so please let me know.

You can use the tactical "Info" for this: "Info <tac>" performs <tac> but
also prints what it actually did. Then you can decide to backtrack and
replace <tac> by the actual script (faster) or not (more robust in some
cases).

Notice that this operation is done automatically (try Auto, if it
succeed then replace Auto by the actual script otherwise do nothing)
by the "blast mode" of the pcoq interface
(http://www-sop.inria.fr/lemme/pcoq/index.html).

There are other means to speed up Auto:

 - by separating hint databases (typically have a "light" hint
   database and a "heavy" one). 
 - by using the "Hint Extern" stuff with costs attached to each tactic.


Sincerly,

Pierre Courtieu