Up – Package index » coq-core » Library coq-core.vernac » ComInductive » Internal

Module `ComInductive.Internal`Source

val inductive_levels : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr list ->
  EConstr.rel_context list list ->
  Evd.evar_map * EConstr.t list

Returns the modified arities (the result sort may be replaced by Prop). Should be called with minimized universes.