coq - 由于 CoQ Tatic 故障（可逆一阶模式）和错误的项目符号导致生成 *.vos 文件的问题

Question

每次我尝试使用 CoqIDE 编译器 (v8.13.2) 编译在此链接上找到的 CoQ 描述时，都会显示以下错误消息

795: Tactic failure: reversible in 1st order mode.
800: Tactic failure: reversible in 1st order mode.
893: [Focus] Wrong bullet +: Current bullet + is not finished.
904: The reference h was not found in the current environment.

我遇到了CoQ 问题日志中描述的战术失败的潜在解决方案。但是，我不知道如何正确应用它。

此外，我不确定与错误项目符号相关的问题是否是上述问题的结果。