Internal (rocq-runtime.Rewrite.Internal)

val build_signature : Environ.env -> Evd.evar_map -> EConstr.constr -> (EConstr.types * EConstr.types option) option list -> (EConstr.types * EConstr.types option) option -> Evd.evar_map * EConstr.constr * (EConstr.constr * EConstr.t option) list

val build_morphism_signature : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.t

val default_morphism : Environ.env -> Evd.evar_map -> ((EConstr.types * EConstr.types option) option list * (EConstr.types * EConstr.types option) option) -> EConstr.constr -> EConstr.constr * EConstr.t