Expand (rocq-runtime.Evd.Expand)

type handle

val empty_handle : handle

val liftn_handle : int -> handle -> handle

val kind : 
  evar_map ->
  handle ->
  econstr ->
  handle
  * (econstr,
      econstr,
      MiniEConstr.ESorts.t,
      MiniEConstr.EInstance.t,
      MiniEConstr.ERelevance.t)
      Constr.kind_of_term

val expand : evar_map -> handle -> econstr -> econstr

val expand_instance : 
  skip:bool ->
  undefined evar_info ->
  handle ->
  econstr SList.t ->
  econstr SList.t