• Andrei Paskevich's avatar
    switch Typing to the new Dterm-based API · 460e93f8
    Andrei Paskevich authored
    - Make [Highord.pred 'a] an alias for [Highord.func 'a bool],
    rename [Highorg.(@!)] to [(@)], remove [Highorg.(@?)], remove
    the quantifiers [\!] and [\?] and only leave [\] which is the
    only true lambda now;
    - Allow mixing bool and Prop in logic, Dterm will introduce
    coercions where necessary (trying to minimize the number of
    if-then-else in the term context).
ocaml.drv 1.06 KB