vellvm / ctrees

An itree-like data-structure to additionally support internal non-determinism
MIT License
13 stars 2 forks source link

Porting the library to 8.15, coq-coinduction's latest changes, and speeding up compilation #9

Closed YaZko closed 2 years ago

YaZko commented 2 years ago

This PR moves in a non-retrocompatible way toward coq 8.15 and the latest version of coq-coinduction.

Be sure to perform a git pull & opam upgrade . in your local clone of coq-coinduction.

The coq-relational-algebra library can now simply be installed via opam -- or switch to the v8.15 branch on your local clone otherwise.

We now depend on coq-equations, available on Opam.