Remove need for parentheses in many places

[pimotte]

Fixes #115

TODO:

• Replace Notation hacks by proper solution? Document hack, because ocaml API needed is in Coq 8.18
• Update waterproof-exercises Companion PR
• Fix make build
• Also make Choose a. work instead of Choose (a). Leave Choose (a). as-is.

[jim-portegies]

I think this looks great! It's really a large improvement.

One question: As a test and for the looks of it, it may be nice to also remove parentheses in library files, although this is not strictly necessary. What's your view on this?

[pimotte]

I think this looks great! It's really a large improvement.

One question: As a test and for the looks of it, it may be nice to also remove parentheses in library files, although this is not strictly necessary. What's your view on this?

I removed them incidentally, largely when I was touching stuff to add "as". I guess it would help to detect issues like the disjoint set ambiguity, so I'll probably remove more.

[pimotte]

The reason Choose a. doesn't work is because it's expecting the continuation :=: Choose a := ....

Some options:

• Leave Choose (a). as-is. It's not heavily used currently.
• Reword Choose (a). as We show a works. or something similar.
• Disable Choose (a). in favour of Choose a0 := a.

My gut feeling is towards the second option, but I might be missing some other option to resolve the parsing ambiguity. @jim-portegies any thoughts?

[jim-portegies]

I'm leaning towards option 3. I don't mind 1 either. I am not the biggest fan of 2 because in principle I would like to communicate one way of doing things.

[pimotte]

Fair enough. From an engineering point of view, I'd like to then go with option 1 for this PR, we can then follow up with option 3 if we feel it's worth it.

[pimotte]

With some refactoring we might also be able to do Choose a. (currently, the way the parsing is structured is that the ident := is optional, where instead we might want the := open_lconstr part to be optional.

Edit: After experimenting a bit, I don't think we can do this without disabling Choose _, so in any case I'm delegating investigation to a possible future PR.