Make it possible to enable/disable a String Notation

[gmalecha]

Is your feature request related to a problem?

Currently, regular notations can be enabled and disabled selectively using Disable Notation, but there is no way to do this with String Notation and Number Notation.

Proposed solution

The nicest solution would be to extend the Disable Notation mechanism to support string notations. This seems like it could be done by adding an additional table that tracks whether each string notation is enabled or not.

Wild speculation This table would need to be consulted in uninterp_prim_token to filter the list from prim_token_uninterp_infos. I have not looked into the parsing side.

Alternative solutions

An alternative solution is to make it so that registering an overlapping String Notation overwrites the previous notation. To me, this makes sense as the semantics anyways, but using it for this case requires that you know the name of the parsing/printing function.

Additional context

Additional context here: https://coq.zulipchat.com/#narrow/stream/423352-Coq-Notation-system/topic/Disable.20selective.20literal.20notation