msat

Library containing a SAT solver that can be parametrized by a theory
Library msat.backend
Module Msat_backend . Coq
module type S = Backend_intf.S

Interface for exporting proofs.

module type Arg = sig ... end

Term printing for Coq

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