Functor Dedukti.Make

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.

Parameters:

`S`	:	`Res.S`
`A`	:	`Arg with type formula := S.St.formula and type lemma := S.lemma and type proof := S.proof`

Proof exporting

Currently, exporting a proof means printing it into a file according to the conventions of a given format.

type t

The type of proofs.

val print : Format.formatter -> t -> unit

A function for printing proofs in the desired format.