The Coq mailing list

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

Hello --

I have two questions that are related to writing plugins. If anyone can point me to other plugins or appropriate places in the Coq sources I would greatly appreciate it.

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?

Many thanks.

--

gregory malecha

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