Better template-coq printers

[MathisBD]

This PR improves the pretty-printers in MetaCoq.Template.Pretty : they now handle whitespace and indentation much better (i.e. the output adapts to the screen width), the output syntax is much closer to actual Coq syntax, and pretty-printing is now configurable using a set of options.

This does bring in a dependency on the external library coq-pprint, which is a general-purpose pretty-printing combinator library developed and maintained by myself.

[yforster]

Can you provide a pointer to a file where the improvement becomes evident? Alternatively, maybe add something to the test-suite which prints a couple of things?

[MathisBD]

There is no such file : the template-coq printers are used nowhere in metacoq at the moment. I am personally making great use of them in my own branches (e.g. to print debug traces for unification), which will not be integrated into metacoq before a couple weeks.

[MathisBD]

Yes I can add something to the test-suite that quotes some medium-sized terms and prints them. Are you asking this so that people have a simple example of how to use the new printers ? The test-suite might not be the best place for this :)

[yforster]

I think this would fit perfectly in the examples directory. And yes, I'm asking so people see how to use them, but also to have a place to check whether things broke when we change e.g. the printers in the future