Up – Package index » rocq-runtime » Library rocq-runtime.pretyping » Reductionops » CredNative

Module `Reductionops.CredNative`Source

Sourcetype elem = EConstr.t

Sourcetype args = EConstr.t array

Sourcetype evd = Evd.evar_map

Sourcetype uinstance = EConstr.EInstance.t

val red_prim : 
  Environ.env ->
  evd ->
  CPrimitives.t ->
  uinstance ->
  args ->
  elem option