package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val assumption_of_judgment : Environ.env -> Environ.unsafe_judgment -> Sorts.relevance
val type1 : Constr.types
val type_of_sort : Sorts.t -> Constr.types
val judge_of_prop : Environ.unsafe_judgment
val judge_of_set : Environ.unsafe_judgment
val type_of_relative : Environ.env -> int -> Constr.types
val judge_of_relative : Environ.env -> int -> Environ.unsafe_judgment
val type_of_variable : Environ.env -> Names.variable -> Constr.types
val judge_of_variable : Environ.env -> Names.variable -> Environ.unsafe_judgment
val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.types
val sort_of_product : Environ.env -> Sorts.t -> Sorts.t -> Sorts.t
val type_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * Univ.AUContext.t
val check_hyps_inclusion : Environ.env -> ?evars:(Constr.existential -> Constr.constr option) -> Names.GlobRef.t -> Constr.named_context -> unit
val type_of_int : Environ.env -> Constr.types
val type_of_float : Environ.env -> Constr.types
val judge_of_float : Environ.env -> Float64.t -> Environ.unsafe_judgment
val type_of_array : Environ.env -> Univ.Instance.t -> Constr.types
val warn_bad_relevance_name : string
val should_invert_case : Environ.env -> Constr.case_info -> bool