• Raphael Cauderlier's avatar
    Remove dependency on dktactics/fol · 2bbd2908
    Raphael Cauderlier authored
    Depending on dktactics makes writing the interoperability layer hard
    because most types in dktactics are not definable.
    
    Moreover, this removes dependency on Dedukti v2.6 (featuring injective
    symbols). When the transfer tactic will be called, it will not know
    about the rule [a,b] term (arr a b) --> term a -> term b.
    2bbd2908