Internal (p.coq-core.8.18.0.doc.coq-core.tactics.Rewrite.Internal)

Source

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

Source

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

Source

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