The Coq mailing list

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

On Thu, Jun 18, 2015 at 06:43:34PM +0200, Christian Doczkal wrote:
> Is this a temporary measure, or is there a principled reason why this
> cannot work in Coq 8.5? I someties use this in combination with Print
> Assumptions to get a quick overview of all the "holes" in some
> theorem.

Hello, there is indeed a technical reason why generating Axioms on the
fly in the middle of a proof (what 8.4 admit was doing) cannot work
anymore.

If you want an admit tactic as in 8.4 you need to do the following

  Axiom devil : False.
  Ltac admit := case devil.

Unfortunately Print Assumptions will simply display this axiom instead of
all its uses (i.e. which type was inhabited by using the devil axiom).
There is an open bug in the bug tracker, It will be fixed for 8.5.

Just for the records, the standard admit tactic in 8.5 lets you give up
goals.  When you close all the non given up ones, Coq prints the goals
you did not solve.

Best,
-- 
Enrico Tassi