Is there a way to disable a specific notation in Coq?

Question

I'd like, in Coqide, to have the proof state not use a certain notation (but still use all others).

Is this possible?

Answer 1

Some tricks that might be sufficient are described here: How to disable my custom notation in Coq?

I wanted to add pointer to that answer because this question comes up first on Google.

Answer 2

From what I understand in the documentation, it is not possible. You might be able to play with opening/closing scopes but I'm not sure it will work, since it is stated explicitly that notations will be used for printing whenever possible.