Previous  Up  Next

Module Coq.Equivalence

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