Module AAC_coq.Transitive

module Transitive: sig .. end

val make : Term.constr -> Term.constr -> Term.constr -> t

val infer : AAC_coq.goal_sigma ->
       Term.constr -> Term.constr -> t * AAC_coq.goal_sigma

val from_relation : AAC_coq.goal_sigma ->
       AAC_coq.Relation.t -> t * AAC_coq.goal_sigma

val cps_from_relation : AAC_coq.Relation.t ->
       (t -> Proof_type.tactic) -> Proof_type.tactic

val to_relation : t -> AAC_coq.Relation.t