Module `Msat_backend.Coq`

module type Arg = sig ... end

module Make : functor (S : Msat.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

module Simple : functor (S : Msat.S) -> functor (A : Arg with type hyp = S.formula list and type lemma := S.lemma and type assumption := S.formula) -> S with type t := S.proof: Simple functor to output Coq proofs