The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

A "simple" solution could be to use memoization to save time: until
the tactique language is deterministic the result of an user defined
tactinque can be saved and cached... i think it will rule out the big
majority of delays in coq script maintainance.