The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

A (quite comprehensive) list of examples of plugins I know of:

- https://github.com/braibant/Timing-plugin (this one is quite simple,
but quite useful for timing tactics)
- http://coq.inria.fr/cocorico/evar_match (now integrated in 8.4, but
nicely commented)
- https://github.com/mattam82/Constructors (not updated for the new
coq_makefile)
- http://coq.inria.fr/cocorico/UnfoldFixpointOnce
- https://github.com/braibant/coq-tutorial-ml-tactics (tutorial on 
reification)
- https://github.com/tomprince/rippling (proof automation)
- http://sardes.inrialpes.fr/~braibant/aac_tactics/ (rewriting modulo AC)
- ssreflect (http://www.msr-inria.inria.fr/Projects/math-components)

Reading through the ml code of these may give leads about what to
search for (and I really think that _not_ opening  modules would help
a lot to find where things are defined).

>        let consts = pe.Pre_env.env_globals.Pre_env.env_constants in
(is backward compatibility with OCaml 3.11 worth it when writing
plugins ? If not, then

let consts = Pre_env.( pe.env_globals.env_constants ) in

is more palatable.)

Hope this helps,
Thomas