The Coq mailing list

[Christian Doczkal <christian.doczkal AT uni-saarland.de>]

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? I someties use this in combination with Print Assumptions to 
get a quick overview of all the "holes" in some theorem.

-- 
Regards
Christian