package rocq-runtime

  1. Overview
  2. Docs

Module CbvSource

Sourcetype cbv_infos

Entry point for cbv normalization of a constr

Sourceval create_cbv_infos : RedFlags.reds -> strong:bool -> Environ.env -> Evd.evar_map -> cbv_infos