The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Your suggest works fine and is obvious a good way to proceed, however
it left the problem of when you was thinking something to be NOT
allowed, or not provable,
and instead it is.
Can looking in proofs flows helps for that? It looks like, but may be
I'm not enough coq-expert to say something about.