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
val constrained_type_of_inductive : Environ.env -> mind_specif Univ.puniverses -> Constr.types Univ.constrained
val constrained_type_of_inductive_knowing_parameters : Environ.env -> mind_specif Univ.puniverses -> Constr.types Lazy.t array -> Constr.types Univ.constrained
val type_of_inductive : Environ.env -> mind_specif Univ.puniverses -> Constr.types
val type_of_inductive_knowing_parameters : Environ.env -> ?polyprop:bool -> mind_specif Univ.puniverses -> Constr.types Lazy.t array -> Constr.types
val elim_sorts : mind_specif -> Sorts.family list
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 -> Constr.case_info -> unit
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.constr array -> Constr.constr array