Make sure that when you lift something into a context that has already been completed, that terms or theorems containing unqualified constants cannot be lifted. This is probably not a bug that can be exploited in ProofScript currently, but one that could be exploited with direct access to the kernel.
Make sure that when you lift something into a context that has already been completed, that terms or theorems containing unqualified constants cannot be lifted. This is probably not a bug that can be exploited in ProofScript currently, but one that could be exploited with direct access to the kernel.