Module type Coq.S

Interface for exporting proofs.

type t

The type of proofs.

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

A function for printing proofs in the desired format.