The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users and Team,

recent versions of Coq give this message when proofs are nested (a new Lemma 
is started inside of a proof)

"Nested proofs are deprecated and will stop working in the next Coq version"

I would like to have a discussion on this because I use this regularly. I 
like a heavily automated proof style and when automation gets stuck, I tend 
to solve this by providing some additional idea in a new lemma and add this 
to the hint database. It makes sense to do this inline/nested for 2 reasons:

- it is quicker (at least during proof development) in case the automation 
did laboriously crunch through a few 100 cases successfully and left over 
only 1 or 2. 
- It documents why you are proving this lemma, which sometimes states 
something which is fairly unmotivated without looking at the proof state at 
this point.

 What do others think about this feature?

What are the reasons for dropping it?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928