Please adapt CompCert to work with https://github.com/coq/coq/pull/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 https://github.com/coq/coq/pull/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!