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

Module `ComInductive.Internal`Source

val compute_constructor_level : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_context ->
  Sorts.t

Sourceval warn_bad_set_minimization : ?loc:Loc.t -> unit -> unit