Pre-compiled binaries (attempt to solve common problems with Coq plugins)


When attempting to use a plugin with a standard installation of coq, you may have the problem that the compiled plugin is not provided for your linux distribution. This page attempts to provide a few pre-compiled versions of plugins for common combinations of versions for Coq and the underlying ocaml system.


If you have a version of Coq on your Linux machine so that the answer to coqtop --version has the following shape (the date is irrelevant)

The Coq Proof Assistant, version 8.2pl1 (August 2009)
compiled on Aug 05 2009 17:41:33 with OCaml 3.11.1+rc1
then you can use this version of ssreflect.

installing HoTT and compiling

try using this script