The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Mar 11, 2013 at 07:56:04AM -0400, Adam Chlipala wrote:
> This approach makes it harder to use [Print Assumptions] to take
> stock of the assumptions a proof depends on.

Well, a patch to make "Print Assumptions qualid" render all the
occurrences of "match daemon return P with end" as "Axiom foo_admitted$N :
P" is not that hard to write.

PS. I'm subscribed to the list.
-- 
Enrico Tassi