Internal (p.coq-core.8.20.1.doc.coq-core.vernac.ComInductive.Internal)

Source

val inductive_levels : 
  Environ.env ->
  Evd.evar_map ->
  poly:bool ->
  indnames:Names.Id.t list ->
  arities_explicit:bool list ->
  EConstr.constr list ->
  EConstr.rel_context list list ->
  Evd.evar_map * (DeclareInd.default_dep_elim list * EConstr.t list)

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

Source

val error_differing_params : 
  kind:string ->
  (Names.lident * Vernacexpr.inductive_params_expr) ->
  (Names.lident * Vernacexpr.inductive_params_expr) ->
  'a

Sourceval do_auto_prop_lowering : bool ref