The Coq mailing list

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

Hi Abhishek,

It would certainly be easy. For instance, to remove all the
associativity/precedence of (only) notations, there is a two-line
patch (replace "prec" with "Prec 0" in cases "UnpMetaVar" and
"UnpLstMetaVar" of "Ppconstr.print_hunks"). You then need to bind this
to an option as done e.g. for "Set Printing All" in
vernacentries.ml. A GitHub Pull Request will then be welcome!

Best,

Hugo

On Thu, Feb 20, 2020 at 11:00:32AM -0800, Abhishek Anand wrote:
> Would it be easy to implement this feature in Coq to ignore all the
> associativity/precedence smarts and print all the parentheses explicitly?
> It seems many people would like to use such a feature:
> https://stackoverflow.com/questions/39843485/
> can-i-force-coq-to-print-parentheses/39848168
> 
> Unset Printing All is often not useful in these cases because it dumps too 
> much
> information making things unreadable again.
> 
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/