Этот код предназначался для сборки с исправленной пользователем версией Coq 8.4 или Coq 8.3, которая отключала проверку юниверса; Я помню, как разговаривал с Дэном Грейсоном или Владимиром в какой-то момент в то время, и они упоминали, что использовали такую исправленную версию Coq. (Обратите также внимание, что файл взят с августа 2012 года, и 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.