• Andrei Paskevich's avatar
    get rid of user-supplied ty_base · cbf0cede
    Andrei Paskevich authored
    What was its purpose in the first place? Integers are protected
    in Simplify anyway and then we can simply forget the difference
    between the infinite sorts (as we do in encoding_tptp).
    cbf0cede
libencoding.ml 9.44 KB