You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.