The Coq mailing list

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

Dear Maxime,

if I remember right, we had a discussion on the topic during the Coq 
Implementers Workshop in Nice last year. I think you said that the main 
difficulty with nested proofs is that they may depend on the local context 
(the context of the outer proof). I also use nested proofs frequently, but I 
don't use nested proofs which depend on the local context, that is which 
could not be moved in front of the outer lemma. Since Andrew said he usually 
moves the proofs outside eventually, I guess he also doesn't use nested 
lemmas which depend on the local context. Maybe Adam and other friends of 
this feature can comment on their usage.

In cases others agree to this, would it be an option to remove support for 
nested lemmas which depend on the current context? I don't see how this would 
be in any way more complicated than parallel proofs - essentially it should 
be the same. Also I think removing the feature that a nested lemma can depend 
on the outer proof's context would be even an advantage, because I would 
think most people who use this feature use it accidentally and not willingly.

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
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928