Module Dedukti

module Dedukti: sig .. end

Deduki backend for proofs

Work in progress...

module type S = Backend_intf.S

module type Arg = sig .. end

module Make: functor (S : Res.S) -> functor (A : Arg 
          with type formula := S.St.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.