In order to avoid getting noise from user defined notations, I’d like to know if there is a way at the moment to ask Coq to display a fully rewritten vernac command, unrolling all notations. Just to be clear, I don’t want the result of the command to be displayed without notation (there are
For example, If I input
Print (3 + 4)., I’d like to get
Print (plus (S (S (S O))) (S (S (S (S 0)))). as a result.
I don’t know if this already exists. If it is not the case, what would be the best way to achieve that ? A Coq plugin ? Extracting the Notation mechanism in a third-party tool ?
All ideas are welcome