Coq (u.e48875f008bd120f24d497e3f3fa21b2.msat.0.8.3.doc.msat.backend.Msat

Sourcemodule type S = Backend_intf.S

Interface for exporting proofs.

Sourcemodule 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

Source

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