Functor Coq.Simple

module Simple: functor (S : Res.S) -> functor (A : Arg  with type hyp = S.St.formula list
                                  and type lemma := S.lemma
                                  and type assumption := S.St.formula) -> S  with type t := S.proof

Simple functo to output Coq proofs

Parameters:

`S`	:	`Res.S`
`A`	:	`Arg with type hyp = S.St.formula list and type lemma := S.lemma and type assumption := S.St.formula`

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.