Open
Description
I clone the repo and follow the instruction "make querystructures" to build the SQL-like library, but it fail, the error message is below
COQC src/QueryStructure/Specification/SearchTerms/ListInclusion.v
Warning: The -require option is deprecated, please use -require-import
instead. [deprecated-boot,deprecated]
File "./src/QueryStructure/Specification/SearchTerms/ListInclusion.v", line 49, characters 2-140:
Error: Unsolved obligations remaining.
Makefile.coq:677: recipe for target 'src/QueryStructure/Specification/SearchTerms/ListInclusion.vo' failed
make: *** [src/QueryStructure/Specification/SearchTerms/ListInclusion.vo] Error 1
my system is Ubuntu 16.04, my "coqc -v" output is
The Coq Proof Assistant, version 8.11.0 (March 2020)
compiled on Mar 23 2020 4:55:38 with OCaml 4.07.1
Metadata
Metadata
Assignees
Labels
No labels