Module AAC_coq.Transitive


module Transitive: sig .. end


type t = {
   carrier : Term.constr;
   leq : Term.constr;
   transitive : Term.constr;
}
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