sig
type t = {
carrier : EConstr.constr;
eq : EConstr.constr;
equivalence : EConstr.constr;
}
val make :
EConstr.constr -> EConstr.constr -> EConstr.constr -> Coq.Equivalence.t
val infer :
Environ.env ->
Evd.evar_map ->
EConstr.constr -> EConstr.constr -> Coq.Equivalence.t * Evd.evar_map
val from_relation :
Environ.env ->
Evd.evar_map -> Coq.Relation.t -> Coq.Equivalence.t * Evd.evar_map
val to_relation : Coq.Equivalence.t -> Coq.Relation.t
val split :
Coq.Equivalence.t -> EConstr.constr * EConstr.constr * EConstr.constr
end