Skip to content

Fail to make querystructures on Coq > 8.9 #36

Description

@sqrta

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

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions