CVE-2020-37268

A flaw was found in Coq and Rocq provers. The Print Assumptions feature, which is used to audit the soundness of proofs, fails to report when a definition was created without proper "universe checking" a mechanism to ensure logical consistency. This occurs when the definition is incorporated...