Waterproof proof mode: first prototype.

[ejgallego]

Joint work with Gaëtan Gilbert, Pim Otte, Jim Portegies.

[SkySkimmer]

I rebased the submodules, using an indirection to avoid the need to the "hack table".
The rocq version is then ltac2 custom entries + better parsing errors + Ltac2 Default Notation Entry and Ltac2 Default Notation Entry Level
(Ltac2 Default Notation Entry doesn't work great with the now qualified custom entry names but it still works)

instead of those options we may want to have our own Waterproof Notation command wrapping Ltac2 Notation?

[SkySkimmer]

(NB the hack table may have nicer Print Grammar output so maybe we want to put it back?)

[pimotte]

@SkySkimmer Would having a Waterproof Notation command remove the restriction on importing Ltac2 after Waterproof? If yes, then I'm definitely in favour of having this command. If no, then I'm happy to defer to whatever you think is best.

With respect to the hack table: Depends a bit on how bad the grammar gets. In any case, the output we had from print grammar was already slightly lacking in the sense that we had to manually reverse engineer the parse tree, so that's actually what we would want. In any case, all of this is for developers only, so I have no strong preference, again happy to defer to what you think is best:)

[SkySkimmer]

I don't remember what the restriction was exactly, but importing Ltac2 after Waterproof would still change the default proof mode at least.

[SkySkimmer]

I rebased the submodules, using an indirection to avoid the need to the "hack table".

seems I didn't push to the right place, the rebase is at https://github.com/impermeable/waterproof-dev/tree/wp_proof_mode

[SkySkimmer]

continued in #9