GitLab

This printer can be used to test the Albert’s parser.

The "IF_RIGHT" instruction has been removed from Mi-Cho-Coq in commit
e729117e3be1159550944b43b094ae54d9183dc1

`DROP1` at pattern position was interpreted as an unused variable
instead of `DROP 1`. This lead to eagerly replacing `PUSH ty x;
<anything>` by `NOOP`, which is incorrect.

This bug was probably introduced during the adaptation to Babylon.

These "partial proofs" would will need to be adapted to the syntax updates,
they eat a lot of compilation time and ends up to prove nothing as
they are admitted.