To run in coq-8.1, use absint81.v To run in coq-8.2, use absint.v (tested with coq-8.2beta4)