Proof obligations generated, but not in the proof mode

[pi8027]

The Parametricity Recursive command says "The parametricity tactic generated generated proof obligations. Please prove them and end your proof with 'Parametricity Done'". But it does not open the proof mode. For example, the code shown in #4 (comment) fails at intros immediately after Parametricity Recursive Gcd with a syntax error. Also, Parametricity Done fails with "Error: Command not supported (No proof-editing in progress)".

I had this issue with both paramcoq.1.1.2+coq8.13 and paramcoq.dev.

[proux01]

Thanks for reporting. This is indeed broken since Coq 8.10 (IIRC). I tried using the obligation mechanism but this is non trivial and since nobody was using it, this is still not fixed.

Meanwhile, the only solution is to look at the proof obligation (coqtop still displays it IIRC) and modify the Parametricity Tactic to solve it.