The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Jason Gross 
<jasongross9 AT gmail.com>
 writes:

   I've thrown together a bit of code at
   https://github.com/JasonGross/coq-bug-finder which does some basic

It would be nice if your tool could also be used to create
minimal examples for bugs in Coq specifications. 

For example, I have a universe inconsistency error within a
development of 10,000 lines. I would be really interested to
strip this down to the minimal set of definitions/lemmas that
reproduce the universe inconsistency.

Bye,

Hendrik