coq - 所有子目标均已满足，但无法集中证明

Question

我完成了一个有点冗长的证明，但每当我尝试时，Qed我都会收到错误消息Error: This proof is focused, but cannot be unfocused this way。有没有其他方法可以使证明失去焦点？即使我的证明是严格的，我应该只使用承认吗？作为参考，我使用的是 CoqIDE 8.6

Answer 1

解决了，我在证明结尾处遗漏了一个“}”。