package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type uniform_inductive_flag =
  1. | UniformParameters
  2. | NonUniformParameters
val do_mutual_inductive : template:bool option -> Constrexpr.cumul_univ_decl_expr option -> (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> cumulative:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags -> private_ind:bool -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit
val make_cases : Names.inductive -> string list list
val interp_mutual_inductive_constr : sigma:Evd.evar_map -> template:bool option -> udecl:UState.universe_decl -> variances:Entries.variance_entry -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> indnames:Names.Id.t list -> arities:EConstr.t list -> arityconcl:(bool * EConstr.ESorts.t) option list -> constructors:(Names.Id.t list * Constr.constr list) list -> env_ar_params:Environ.env -> cumulative:bool -> poly:bool -> private_ind:bool -> finite:Declarations.recursivity_kind -> Entries.mutual_inductive_entry * UnivNames.universe_binders
val should_auto_template : Names.Id.t -> bool -> bool
val template_polymorphism_candidate : ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool
val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int -> EConstr.t -> Evd.evar_map
val variance_of_entry : cumulative:bool -> variances:Entries.variance_entry -> Entries.universes_entry -> Entries.variance_entry option