sig
  type t = {
    carrier : Term.constr;
    leq : Term.constr;
    transitive : Term.constr;
  }
  val make : Term.constr -> Term.constr -> Term.constr -> Coq.Transitive.t
  val infer :
    Coq.goal_sigma ->
    Term.constr -> Term.constr -> Coq.Transitive.t * Coq.goal_sigma
  val from_relation :
    Coq.goal_sigma -> Coq.Relation.t -> Coq.Transitive.t * Coq.goal_sigma
  val cps_from_relation :
    Coq.Relation.t ->
    (Coq.Transitive.t -> Proof_type.tactic) -> Proof_type.tactic
  val to_relation : Coq.Transitive.t -> Coq.Relation.t
end