The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Thanks. This is really helpful.

On Sun, Aug 24, 2014 at 4:45 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

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

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/