search

uwdb / Cosette

Cosette is an automated SQL solver.
BSD 2-Clause "Simplified" License
662 stars 54 forks source link

Building hott for Coq results in "Unable to satisfy the following constraints" error #66

Closed adaszews closed 6 years ago

adaszews commented 6 years ago

Scenario:

1) set up the necessary prerequisites 2) go to Cosette/hott/ 3) type make

Expected:

hott module for Coq should complete building successfully

What happens:

make[1]: Entering directory `/pstore/home/adaszews/Cosette/hott/.build' COQC library/UnivalentSemantics.v COQC .build_solve/library/UnivalentSemantics.v File "./library/UnivalentSemantics.v", line 10, characters 2-57: Error: Unable to satisfy the following constraints: In environment: T : type

?Denotation : "Denotation type Type"

adaszews commented 6 years ago

NVM, with coq-HoTT it works, I think I've been using vanilla coq