Fix the FPA support for the legacy frontend

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo

https://alt-ergo.ocamlpro.com/

Other

130 stars 33 forks source link

Closed Halbaroth closed 4 months ago

Halbaroth commented 4 months ago

The FPA support have been broken on next for the legacy frontend. For instance, the following input file isn't typechecked anymore:

logic x : fpa_rounding_mode
logic y : real
logic z : real

goal g : y = z

This commit fixes the old typechecker.