search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

The reference X0 was not found in the current environment #16

Closed vonavi closed 3 years ago

vonavi commented 4 years ago

Hi guys! I ran make and got the following error:

File "./Structure/Limit/Kan/Extension.v", line 65, characters 17-19:
Error: The reference X0 was not found in the current environment.

Coq version is 8.9.0.

Best regards, Vladimir.

dwarfmaster commented 4 years ago

I have the same error (with coq 8.9.1). However if you just remove it from the list of files to compile in _CoqProject and recreate the makefile, you can compile and use the rest of the library just fine.

jwiegley commented 3 years ago

category-theory now requires at least 8.10, though most of the files may still work with 8.9.