verse-lab / toychain

A minimalistic blockchain consensus implemented and verified in Coq
BSD 2-Clause "Simplified" License
111 stars 12 forks source link

Rely on HTT library from IMDEA instead of Heaps directory #10

Closed palmskog closed 6 years ago

palmskog commented 6 years ago

Instead of maintaining a fork of the Hoare Type Theory (HTT) library, depend on a release of the library in the same way as depending on ssreflect (e.g., via OPAM). I have submitted a pull request that makes HTT more packaging friendly as a first step.

palmskog commented 6 years ago

Solved by #16.