package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Evd.Expand`Source

Only used as EConstr internals

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

package rocq-runtime

Module Evd.ExpandSource

Module `Evd.Expand`Source