avoid deprecated Proof <term>.
I didn't even know this was a thing, and it seems the Coq devs consider it deprecated and won't fix the issues it has (it doesn't properly work in ProofGeneral).
I didn't even know this was a thing, and it seems the Coq devs consider it deprecated and won't fix the issues it has (it doesn't properly work in ProofGeneral).