Module Coq.Classes

module Classes: sig .. end
Coq typeclasses

val mk_morphism : EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
val mk_equivalence : EConstr.constr -> EConstr.constr -> EConstr.constr
val mk_reflexive : EConstr.constr -> EConstr.constr -> EConstr.constr
val mk_transitive : EConstr.constr -> EConstr.constr -> EConstr.constr