Functor Coq.Make

module Make: functor (S : Res.S) -> functor (A : Arg  with type hyp := S.clause
                                and type lemma := S.clause
                                and type assumption := S.clause) -> S  with type t := S.proof

Base functor to output Coq proofs

Parameters:

`S`	:	`Res.S`
`A`	:	`Arg with type hyp := S.clause and type lemma := S.clause and type assumption := S.clause`

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.