Skip to content
  • Raphael Cauderlier's avatar
    Remove dependency on dktactics/fol and add Coq import · 82916e9e
    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.
    82916e9e