Porting from `omega` to `lia`
This is in preparation of https://github.com/coq/coq/pull/7878 and is backward compatible (tested on Coq master, expected to build on 8.8).
The patch rebinds omega
to lia
on the Flocq side and fixes all the
incompatibilities due to scripts relying on incompleteness of omega
(no occurrence of lia
being weaker were found).
Porting the 30000 lines of Pff.v
was quite painful. My IDE (and wrist) barely survived it. Is there a reason for having such a monolithic file?