The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 03/11/2013 06:56 AM, Enrico Tassi wrote:
> The admit tactic is just implemented as "case daemon" where daemon is
> an Axiom of False.  Again no side effects (no axiom injected into the
> environment by the tactic).
>    

From the department of unintended consequences...

This approach makes it harder to use [Print Assumptions] to take stock 
of the assumptions a proof depends on.