package coq

  1. Overview
  2. Docs
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) * UGraph.t) -> ('a -> Constr.constr) -> 'a -> Constr.named_context -> unit
val check_primitive_type : Environ.env -> CPrimitives.op_or_type -> Constr.types -> 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_prim_type : Environ.env -> CPrimitives.prim_type -> Constr.types
val type_of_prim : Environ.env -> CPrimitives.t -> Constr.types
val warn_bad_relevance_name : string
OCaml

Innovation. Community. Security.