-
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