C'è un modo per disabilitare una notazione specifica in Coq?

Question

Vorrei che, in Coqide, lo stato di prova non usasse una certa notazione (ma usassimo ancora tutte le altre).

È possibile?

Answer 1

Da quanto ho capito nella documentazione, non è possibile. Potresti essere in grado di giocare con gli ambiti di apertura/chiusura, ma non sono sicuro che funzionerà, dal momento che si afferma esplicitamente che le notazioni saranno utilizzate per la stampa, quando possibile.

Answer 2

Alcuni trucchi che potrebbero essere sufficienti sono descritte qui: How to disable my custom notation in Coq?

Volevo aggiungere puntatore a tale risposta, perché questa domanda arriva prima su Google.