Module Coq.Simple

Parameters

• S : Msat.S
• A : Arg with type hyp = S.formula list and type lemma := S.lemma and type assumption := S.formula

Signature

type t

The type of proofs.

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

A function for printing proofs in the desired format.