Confusing error message for floating-point literals
theory T use ieee_float.Float32 as B32 goal g : (1.:B32.t) = (1:B32.t) end
Type t cannot be used for a numeric literal, which is wrong by definition.
Either the error message should be
Invalid floating point literal: '1', or the code should just be modified to accept such a literal.