Module Sig

module Sig: sig .. end

type answer =

`\|`	`Yes of Explanation.t`
`\|`	`No`

type 'a literal =

`\|`	`LSem of 'a Literal.view`
`\|`	`LTerm of Literal.LT.t`

type 'a input = 'a Literal.view * Literal.LT.t option * Explanation.t

type 'a result = {

	`assume : ('a literal * Explanation.t) list;`
	`remove : ('a literal * Explanation.t) list;`

}

module type RELATION = sig .. end

module type THEORY = sig .. end

module type COMBINATOR = sig .. end

module type X = sig .. end

module type C = sig .. end