Require Import ZArith before using it in ModularArithmeticTheorems.v (for coq/coq#19801) - Githubissues

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat

http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf

Other

717 stars 147 forks source link

Require Import ZArith before using it in ModularArithmeticTheorems.v (for coq/coq#19801) #1979

Closed andres-erbsen closed 2 weeks ago