package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val find_inductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val find_coinductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val lookup_mind_specif : Environ.env -> Names.inductive -> mind_specif
val instantiate_inductive_constraints : Declarations.mutual_inductive_body -> Univ.Instance.t -> Univ.Constraint.t
type param_univs = (unit -> Univ.Universe.t) list
val make_param_univs : Environ.env -> Constr.constr array -> param_univs
val constrained_type_of_inductive : mind_specif Univ.puniverses -> Constr.types Univ.constrained
val constrained_type_of_inductive_knowing_parameters : mind_specif Univ.puniverses -> param_univs -> Constr.types Univ.constrained
val relevance_of_inductive : Environ.env -> Names.inductive -> Sorts.relevance
val type_of_inductive : mind_specif Univ.puniverses -> Constr.types
val type_of_inductive_knowing_parameters : ?polyprop:bool -> mind_specif Univ.puniverses -> param_univs -> Constr.types
val elim_sort : mind_specif -> Sorts.family
val is_private : mind_specif -> bool
val is_primitive_record : mind_specif -> bool
val constrained_type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types Univ.constrained
val type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types
val arities_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array
val type_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array
val arities_of_specif : Names.MutInd.t Univ.puniverses -> mind_specif -> Constr.types array
val inductive_params : mind_specif -> int
val inductive_sort_family : Declarations.one_inductive_body -> Sorts.family
val check_case_info : Environ.env -> Constr.pinductive -> Sorts.relevance -> Constr.case_info -> unit
val is_primitive_positive_container : Environ.env -> Names.Constant.t -> bool
val check_fix : Environ.env -> Constr.fixpoint -> unit
val check_cofix : Environ.env -> Constr.cofixpoint -> unit
exception SingletonInductiveBecomesProp of Names.Id.t
val max_inductive_sort : Sorts.t array -> Univ.Universe.t
type size =
  1. | Large
  2. | Strict
type subterm_spec =
  1. | Subterm of size * Declarations.wf_paths
  2. | Dead_code
  3. | Not_subterm
type guard_env = {
  1. env : Environ.env;
  2. rel_min : int;
  3. genv : subterm_spec Lazy.t list;
}
type stack_element =
  1. | SClosure of guard_env * Constr.constr
  2. | SArg of subterm_spec Lazy.t
val subterm_specif : guard_env -> stack_element list -> Constr.constr -> subterm_spec
val lambda_implicit_lift : int -> Constr.constr -> Constr.constr
val abstract_mind_lc : int -> Int.t -> (Constr.rel_context * Constr.constr) array -> Constr.constr array