The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

On 25 juin 2012, at 17:03, Thomas Braibant wrote:

> 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).

Thanks a lot for these links, I've started to go through them (and reading 
how extraction works, because what I want to do seems a little bit related to 
that as well).

Alan