coq 8.7.2 · OCaml Package

val find_rectype : 
  Environ.env ->
  Term.types ->
  Term.pinductive * Term.constr list

val find_inductive : 
  Environ.env ->
  Term.types ->
  Term.pinductive * Term.constr list

val find_coinductive : 
  Environ.env ->
  Term.types ->
  Term.pinductive * Term.constr list

type mind_specif =
  Declarations.mutual_inductive_body * Declarations.one_inductive_body

val lookup_mind_specif : Environ.env -> Names.inductive -> mind_specif

val ind_subst : 
  Names.mutual_inductive ->
  Declarations.mutual_inductive_body ->
  Univ.universe_instance ->
  Term.constr list

val inductive_paramdecls : 
  Declarations.mutual_inductive_body Univ.puniverses ->
  Context.Rel.t

val instantiate_inductive_constraints : 
  Declarations.mutual_inductive_body ->
  Univ.universe_instance ->
  Univ.constraints

val constrained_type_of_inductive : 
  Environ.env ->
  mind_specif Univ.puniverses ->
  Term.types Univ.constrained

val constrained_type_of_inductive_knowing_parameters : 
  Environ.env ->
  mind_specif Univ.puniverses ->
  Term.types Lazy.t array ->
  Term.types Univ.constrained

val type_of_inductive : 
  Environ.env ->
  mind_specif Univ.puniverses ->
  Term.types

val type_of_inductive_knowing_parameters : 
  Environ.env ->
  ?polyprop:bool ->
  mind_specif Univ.puniverses ->
  Term.types Lazy.t array ->
  Term.types

val elim_sorts : mind_specif -> Term.sorts_family list

val is_private : mind_specif -> bool

val is_primitive_record : mind_specif -> bool

val constrained_type_of_constructor : 
  Term.pconstructor ->
  mind_specif ->
  Term.types Univ.constrained

val type_of_constructor : Term.pconstructor -> mind_specif -> Term.types

val arities_of_constructors : 
  Term.pinductive ->
  mind_specif ->
  Term.types array

val type_of_constructors : Term.pinductive -> mind_specif -> Term.types array

val arities_of_specif : 
  Names.mutual_inductive Univ.puniverses ->
  mind_specif ->
  Term.types array

val inductive_params : mind_specif -> int

val type_case_branches : 
  Environ.env ->
  (Term.pinductive * Term.constr list) ->
  Environ.unsafe_judgment ->
  Term.constr ->
  Term.types array * Term.types

val build_branches_type : 
  Term.pinductive ->
  (Declarations.mutual_inductive_body * Declarations.one_inductive_body) ->
  Term.constr list ->
  Term.constr ->
  Term.types array

val mind_arity : 
  Declarations.one_inductive_body ->
  Context.Rel.t * Term.sorts_family

val inductive_sort_family : 
  Declarations.one_inductive_body ->
  Term.sorts_family

val check_case_info : Environ.env -> Term.pinductive -> Term.case_info -> unit

val check_fix : Environ.env -> Term.fixpoint -> unit

val check_cofix : Environ.env -> Term.cofixpoint -> unit

exception SingletonInductiveBecomesProp of Names.Id.t

val max_inductive_sort : Term.sorts array -> Univ.universe

val instantiate_universes : 
  Environ.env ->
  Context.Rel.t ->
  Declarations.template_arity ->
  Term.constr Lazy.t array ->
  Context.Rel.t * Term.sorts

type size =

| Large
| Strict

type subterm_spec =

| Subterm of size * Declarations.wf_paths
| Dead_code
| Not_subterm

type guard_env = {

env : Environ.env;
rel_min : int;
genv : subterm_spec Lazy.t list;

}

type stack_element =

| SClosure of guard_env * Term.constr
| SArg of subterm_spec Lazy.t

val subterm_specif : 
  guard_env ->
  stack_element list ->
  Term.constr ->
  subterm_spec

val lambda_implicit_lift : int -> Constr.constr -> Term.constr

val abstract_mind_lc : 
  int ->
  Int.t ->
  Constr.constr array ->
  Constr.constr array

package coq