Descrição
Provas formais em Coq podem usar a unidade de reflexão em pequena escala do Mathematical Components. O pacote instala a biblioteca de provas ssreflect para Coq, não um programa independente. Ele é útil para usuários de prova de teoremas e desenvolvedores que precisam de lemas e táticas reutilizáveis.