Module Coq

module Coq: sig .. end

Coq Backend

This module provides an easy way to produce coq scripts corresponding to the resolution proofs output by the sat solver.

module type S = Backend_intf.S

Interface for exporting proofs.

module type Arg = sig .. end

module Make: functor (S : Res.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 : Res.S) -> functor (A : Arg  with type hyp = S.St.formula list
                                  and type lemma := S.lemma
                                  and type assumption := S.St.formula) -> S  with type t := S.proof

Simple functo to output Coq proofs