Please adapt CompCert to work with rocq-prover/rocq#17022. A suggested strategy is to add Require Btauto to files that Require ZArith and then fix up the cases where auto is now stronger at using hypotheses such as b = true. Other developments have had a handful of cases like this. Thanks!
Please adapt CompCert to work with rocq-prover/rocq#17022. A suggested strategy is to add
Require Btautoto files thatRequire ZArithand then fix up the cases whereautois now stronger at using hypotheses such asb = true. Other developments have had a handful of cases like this. Thanks!