Module `Msat_backend.Dedukti`

module type S = Backend_intf.S

module type Arg = sig ... end

module Make : functor (S : Msat.S) -> functor (A : Arg with type formula := S.formula and type lemma := S.lemma and type proof := S.proof) -> S with type t := S.proof: Functor to generate a backend to output proofs for the dedukti type checker.