This repository contains the main libraries of Hoare Type Theory (HTT) for reasoning about sequential heap-manipulating programs.
- Coq 8.5pl3 (available from https://coq.inria.fr/coq-85)
- Mathematical Components 1.6.1 (http://math-comp.github.io/math-comp/)
After installing SSReflect, make sure to have the following environment variables properly declared.
make clean; make