我最近在读阿尔瓦罗·佩拉约(Álvaro Pelayo(和迈克尔·A·沃伦(Michael A. Warren(的文章《同伦类型理论和沃沃茨基的单价基础》。有一个配套文件 http://mawarren.net/papers/tutorial.v。我用最新的coq verion 8.8.0编译了它，但遇到了错误。谁能帮我？提前谢谢。
此代码旨在使用禁用宇宙检查的 Coq 8.4 或 Coq 8.3 的自定义修补版本进行构建;我记得当时与Dan Grayson或Vladimir交谈过，他们提到使用这种修补版本的Coq。 (另请注意，该文件来自 2012 年 8 月，https://coq.inria.fr/news/说 Coq 8.4 是在当月发布的。 非常不幸的是，您引用的文章似乎没有在任何地方提到Coq的版本。
在任何情况下，您都可以在 Coq 8.5 及更高版本中构建此文件，方法是将参数-type-in-type传递给coqc或coqtop并添加
Set Asymmetric Patterns.
在文件的顶部。 如果您使用的是 ProofGeneral，则可以添加
(* -*- coq-prog-args: ("-type-in-type") -*- *)
也放在文件的顶部，这样您就不必手动将-type-in-type传递给coqtop。