github.com/coq/opam-coq-archive
Krivine's classical realizability
opam install coq-classical-realizability.8.6.0