The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Michael,

A quick partial answer: the underlying grammar engine of Coq, namely
Camlp5, supports removal of grammar rules but the main Coq executable
does not bind a Coq command to it. It is probably worth to investigate
how to do it, possibly from a plugin, even if some care shall have to
be taken to support undoing the removal (for backtracking), and to
ensure that parts of the notation system which assume the existence of
grammar rule are informed of the removal.

Best,

Hugo

On Sun, Apr 29, 2018 at 09:48:23AM +0000, Soegtrop, Michael wrote:
> 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
>