The Coq mailing list

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

Dear Coq Users,

 

I thought that Close Scope <scope> would make the notations defined for the scope inaccessible such as if they have never been defined. But this doesn’t seem to be the case. The parser tables (what is printed by “Print Grammar constr”) don’t change at all when scopes are opened and closed. As it looks Open/Close scope just change the assignment of definition to a specific syntax, but not the syntax as such. Also when e.g. importing a module in a section, the changes to the parser tables seem to be permanent, even after ending the section.

My question is: is there any way to remove a notation defined in an imported module, so that they are really removed from the parser tables and don’t interfere with other notations?

 

Also I wonder if it wouldn’t be possible to disable productions in the parser dynamically. I guess it would get a bit tricky with argument scopes, but still should be doable without a substantial loss in parser performance.

 

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