package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val infer_v : Environ.env -> Constr.constr array -> Environ.unsafe_judgment array
val assumption_of_judgment : Environ.env -> Environ.unsafe_judgment -> Constr.types
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 sort_of_product : Environ.env -> Sorts.t -> Sorts.t -> Sorts.t
val type_of_product : Environ.env -> Names.Name.t -> Sorts.t -> Sorts.t -> Constr.types
val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.types
val check_hyps_inclusion : Environ.env -> ('a -> Constr.constr) -> 'a -> Constr.named_context -> unit