• Raphael Cauderlier's avatar
    Replace type by Type. · 1dad75e6
    Raphael Cauderlier authored
    The main motivation is to ease integration into higher-order logic
    which would orhterwise require fol.term to be a definable
    symbol (which poses injectivity problems).
    
    This change requires -coc, and the latest (v2.5.1) versions of Dedukti
    and Meta Dedukti (because -coc was not present before in Meta
    Dedukti). fol.term is now defined as the identity over types so it is
    not mandatory to remove it from the developments but fol.type needs to
    be replaced by Type since Dedukti does not allow kind-level
    definitions.
    
    A new bug has been discovered (#21276). It has been triggered by the
    eqcert.match_f_equal_goal function and has required to remove the
    eqcert.f_equal certificate transformer.
    1dad75e6
eqcert.dk 3.46 KB