Skip to main content

ssreflect is a special set of tactics designed to enable small-scale reflection proof methodology in Coq proof assistant.

SSReflect, short for small-scale reflection, is part of Coq standard library since Coq 8.7. Proofs using ssreflect look very different from those using standard tactics.