Description
Formal proofs in Coq can use the small-scale reflection unit from Mathematical Components. The package installs the ssreflect proof library for Coq rather than a standalone program. It is useful to theorem-proving users and developers who need reusable lemmas and tactics.