"No such goal" in utils_list.v
Closed this issue · 2 comments
lbordowitz commented
After running make all, I get the following error
...
COQC Shared/Libs/DLW/Utils/utils_list.v
File "./Shared/Libs/DLW/Utils/utils_list.v", line 815, characters 2-35:
Error: No such goal.
Coq version
$ coqc --version
The Coq Proof Assistant, version 8.11.0 (August 2020)
compiled on Aug 24 2020 18:33:21 with OCaml 4.09.1
I am on branch coq-8.12.
yforster commented
I'm sorry for the trouble! It's most likely the non matching Coq version. Do you have access to Coq 8.12? Alternatively you can try the coq-8.11 branch. Please share any further questions with us, we're eager to help and further improve our installation instructions!
lbordowitz commented
I switched to the coq-8.11 branch and it compiled properly. Thank you.