Expand (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.rocq-runtime.engine.Evd.Expand)

Sourcetype handle

Sourceval empty_handle : handle

Sourceval 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

Sourceval expand : evar_map -> handle -> econstr -> econstr

Source

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