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