Replace the `omega` tactic by `lia`?
Coq 8.12 flags omega
as deprecated. Should Flocq switch to using lia
instead?
I made a quick experiment with the Flocq 3.1 that ships with CompCert. Substituting omega
by lia
and adding a couple of Require Import Psatz
seems to work fine. Tested with Coq 8.8, 8.9, and 8.11.