The Coq mailing list

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

Dear Cedric,

 

I checked some of the lemmas I created as nested lemmas. None of them depends on the proof context explicitly and none of them gets any implicit context dependency added by Coq. When I “Check” the lemmas, they look as expected: no dependency on hypothesis in the proof context of when the lemma was started.

 

So how about disallowing context dependent nested lemmas? Of cause I need dependency on section variables, but not on the current proof context. As far as I understood, the others, who expressed interest in this feature, use it in a similar way.

 

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