The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

I have updated Sean Wilson's rippling plugin for automation of inductive
arguments to work with the tip of 8.3 and trunk branch and have posted
it on github:

https://github.com/tomprince/rippling

It currently requires a patch to coq, to allow invoking auto without the
core database. I have also started to clean it up, so it can now be used
by Requireing the appropriate modules. The interface isn't documented,
and still needs more clean up. Also, the plugin generates reams of debug
output, although this can be turned off by editing the ML code.

  Tom