GitLab

same version

Conflicts:
	interop/arith/Makefile
	interop/arith/natural_coq.fcl
	interop/arith/natural_hol.fcl

coqine has the same basename

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.

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.

The FoCaLiZe development is taken from the work on interoperability
between Coq and HOL used to prove the sieve of Eratosthenes.