module Equivalence:sig
..end
type
t = {
|
carrier : |
|
eq : |
|
equivalence : |
val make : EConstr.constr -> EConstr.constr -> EConstr.constr -> t
val infer : Coq.goal_sigma ->
EConstr.constr -> EConstr.constr -> t * Coq.goal_sigma
val from_relation : Coq.goal_sigma -> Coq.Relation.t -> t * Coq.goal_sigma
val to_relation : t -> Coq.Relation.t
val split : t -> EConstr.constr * EConstr.constr * EConstr.constr