Mentions légales du service

Skip to content

Porting from `omega` to `lia`

Maxime Dénès requested to merge mdenes/flocq:omega-lia into master

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?

Merge request reports