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
lia on the Flocq side and fixes all the
incompatibilities due to scripts relying on incompleteness of
(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?