The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 18/06/2015 18:43, Christian Doczkal wrote:
> Hello
>
> I was just looking at the Changelog for Coq 8.5beta2 and I noticed the 
> following:
>
> - A script using the admit tactic can no longer be concluded by either
>    Qed or Defined. In the first case, Admitted can be used instead. In
>    the second case, a subproof should be used.
>
> Is this a temporary measure, or is there a principled reason why this cannot 
> work in Coq 8.5?

Basically, admit no longer generates a fresh axiom, but instead it 
simply discards the current goal. As a consequence, the final proof term 
still contains holes (and thus is ill-formed), so Qed cannot be used to 
save it.

> I someties use this in combination with Print Assumptions to get a quick overview of 
> all the "holes" in some theorem.

I don't know what is the best way to achieve this, but anything that 
displays the holes of your proof will work. For instance, you could type 
"Show Existentials" just before "Admitted".

In fact, Coq somehow does that for you: "No more, however there are 
goals you gave up. You need to go back and solve them: ...". Hmm... I 
now notice that the message syntax is a bit approximative. I should fix 
that.

Best regards,

Guillaume