Module Coq.Equivalence

module Equivalence: sig .. end

type t = {
   carrier : Term.constr;
   eq : Term.constr;
   equivalence : Term.constr;
}
val make : Term.constr -> Term.constr -> Term.constr -> t
val infer : Coq.goal_sigma ->
Term.constr -> Term.constr -> t * Coq.goal_sigma
val from_relation : Coq.goal_sigma -> Coq.Relation.t -> t * Coq.goal_sigma
val cps_from_relation : Coq.Relation.t ->
(t -> Proof_type.tactic) -> Proof_type.tactic
val to_relation : t -> Coq.Relation.t
val split : t -> Term.constr * Term.constr * Term.constr