The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Sat, Aug 23, 2014 at 11:49:59PM -0400, Gregory Malecha wrote:
> 1) Hooks into the backtracking machinery of Coq's toplevel? In particular,
> I have an imperative map that I want to be able to remove elements from
> when the "add new element" command is undone.
> 
> 2) I would also like to store information (that imperative map) in .vo
> files so that it will be restored when I Require a file that builds one of
> these maps. Is there any convenient way to do this?

Look at library/summary.mli (for 1) and library/libobject.mli (for 2).
A comprehensive example is plugins/setoid_ring/newring.ml4 (look for
from_carrier).  I doubt you need the full complexity of subst_th.

Best,
-- 
Enrico Tassi